Theorem PerfectClosure.mk_zero

Modification history

2024-08-21 18:42
Mathlib/FieldTheory/PerfectClosure.lean
chore(Algebra/Prod): add `Prod.mk_one_one` (#15922) …
Modified PerfectClosure.mk_zeroView on Github →
2023-03-21 13:15
Mathlib/FieldTheory/PerfectClosure.lean
feat: port FieldTheory.PerfectClosure (#2879)
Added PerfectClosure.mk_zeroView on Github →