Commit 2025-02-04 18:27 f70851e4

View on Github →

feat(Algebra/GroupWithZero/Int): add lemmas about Zm0 (#21370)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Basic.lean

added theorem zpow_comm

Created Mathlib/Algebra/GroupWithZero/Int.lean

added theorem WithZero.ofAdd_neg_one_pow_comm

added theorem WithZero.ofAdd_zpow