Theorem AddChar.isNontrivial_iff_ne_trivial
Modification history
2024-03-17 08:48
Mathlib/Algebra/Group/AddChar.lean
refactor(Algebra/Group/AddChar): reimplement using structures (#11375) …
Modified AddChar.isNontrivial_iff_ne_trivialView on Github →