Commit 2022-12-26 16:18 2d48a4ee

View on Github →

chore: golf (#1214)

Estimated changes

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

modified def powersHom

modified def zpowersHom

Modified Mathlib/Algebra/Hom/Equiv/TypeTags.lean

Modified Mathlib/Algebra/Order/WithZero.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

Modified Mathlib/Data/Int/GCD.lean

deleted theorem gcd_nsmul_eq_zero

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

modified def AddAction.toEndHom

Modified Mathlib/GroupTheory/GroupAction/Group.lean