Mathlib v3 is deprecated. Go to Mathlib v4

Theorem zmod.fact_prime_two

Modification history

2021-11-28 20:23
src/number_theory/quadratic_reciprocity.lean
chore(data/nat/prime): `fact (2.prime)` (#10441)
Deleted zmod.fact_prime_twoView on Github →
2021-03-24 16:04
src/number_theory/quadratic_reciprocity.lean
feat(tactic/lint): linter for @[class] def (#6061) …
Added zmod.fact_prime_twoView on Github →