Commit 2023-03-15 14:07 42673620

View on Github →

chore: forward-port leanprover-community/mathlib#17483 (#2884) This forward ports the changes introduced by leanprover-community/mathlib#17483 No change is needed to Mathlib.Data.EReal as the proofs have been golfed in a different way.

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

deleted theorem eq_inv_iff_eq_inv

deleted theorem eq_inv_of_eq_inv

added theorem inv_eq_iff_eq_inv

deleted theorem inv_eq_iff_inv_eq

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

modified theorem inv_eq_zero

Modified Mathlib/Algebra/Order/Group/Abs.lean

Modified Mathlib/Algebra/Periodic.lean

Modified Mathlib/Data/Int/Basic.lean

Modified Mathlib/Data/Real/ConjugateExponents.lean

Modified Mathlib/Data/Real/EReal.lean

Modified Mathlib/Data/Set/Pointwise/Interval.lean