Commit 2024-05-19 09:24 83f2884c

View on Github →

chore: Split Algebra.Group.Conj (#13029) Also generalise Units.exists_iff_ne_zero

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Conj.lean

deleted theorem isConj_iff₀

Created Mathlib/Algebra/GroupWithZero/Conj.lean

added theorem isConj_iff₀

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

modified theorem Units.exists_iff_ne_zero

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/Topology/Algebra/Valuation.lean