Commit 2023-05-11 17:49 e122338e

View on Github →

chore: forward-port leanprover-community/mathlib#18958 (#3920) Match https://github.com/leanprover-community/mathlib/pull/18958

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

added theorem div_mul_cancel'''

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

added theorem Int.cast_mul_eq_zsmul_cast

Modified Mathlib/Algebra/Hom/Units.lean