Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-28 20:23 f684721d

View on Github →

chore(data/nat/prime): fact (2.prime) (#10441)

Estimated changes

Modified src/data/nat/prime.lean

added theorem nat.fact_prime_three

added theorem nat.fact_prime_two

Modified src/logic/basic.lean

Modified src/number_theory/quadratic_reciprocity.lean

deleted theorem zmod.fact_prime_two