Code

prime factorization#2062

Code

Merged

Alizter merged 18 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ps/rr/prime_factorisationAlizter/HoTT:ps/rr/prime_factorisationCopy head branch name to clipboardAug 29, 2024

+477-134

Commits

Commits on Aug 18, 2024

• prime factorisation

  Show description for 1e5f9aa
  Alizter

  committed
  1e5f9aa

Commits on Aug 19, 2024

• Types/Prod: fewer universe vars in prod_empty_l/r; adjust List/Theory

  jdchristensen

  committed
  28ccbaf

• Types/Prod: get rid of a free universe variable in decidable_prod

  jdchristensen

  committed
  1321592

• List/Theory: remove some universe annotations and fix typo

  jdchristensen

  committed
  73b4831

• Nat/Division: simplify proof of prime_factorization

  jdchristensen

  committed
  7e9a44b

Commits on Aug 26, 2024

• modify prime_factorization condition

  Show description for 7ed8566
  Alizter

  committed
  7ed8566

• move iff_equiv and make coercion

  Show description for d9bb286
  Alizter

  committed
  d9bb286

• chnage decidable_iff to take an iff

  Show description for 21a475d
  Alizter

  committed
  21a475d

• add decidability of exists for nat pred with upper bounds on witnesses

  Show description for f636050
  Alizter

  committed
  f636050

• Show IsPrime is a hprop under funext

  Show description for 37191ca
  Alizter

  committed
  37191ca

• tighten not_isprime_iff_iscomposite

  Show description for e816daf
  Alizter

  committed
  e816daf

Commits on Aug 28, 2024

• Fix typo: iff_contradiciton -> iff_contradiction

  jdchristensen

  committed
  a6b91ff

• Types/Sum: simplify a couple of proofs

  jdchristensen

  committed
  8209a09

• Nat/Division: change k to a in one spot

  jdchristensen

  committed
  8bfcd83

• Consolidate iff results in one palce

  Show description for 4e44bd1
  Alizter

  committed
  4e44bd1

• remove moved lemmas

  Show description for 7def66f
  Alizter

  committed
  7def66f

• add further comments about seperation of de morgan laws

  Show description for 31758a0
  Alizter

  committed
  31758a0

Commits on Aug 29, 2024

• Decidable.v: One of De Morgan's laws only needs one arg to be decidable

  jdchristensen

  committed
  a68adca