Commit 2023-01-06 16:39 9940b761

View on Github →

feat: mulLeft is a monoid hom (#1348) Match https://github.com/leanprover-community/mathlib/pull/17900

Estimated changes

deleted theorem Equiv.Perm.coe_pow
modified theorem Equiv.Perm.coe_mul
modified theorem Equiv.Perm.coe_one
added theorem Equiv.Perm.coe_pow
deleted theorem Equiv.Perm.iterate_eq_pow
added theorem Equiv.addLeft_add
added theorem Equiv.addLeft_zero
added theorem Equiv.addRight_add
added theorem Equiv.addRight_zero
added theorem Equiv.inv_addLeft
added theorem Equiv.inv_addRight
added theorem Equiv.inv_mulLeft
added theorem Equiv.inv_mulRight
added theorem Equiv.mulLeft_mul
added theorem Equiv.mulLeft_one
added theorem Equiv.mulRight_mul
added theorem Equiv.mulRight_one
added theorem Equiv.pow_addLeft
added theorem Equiv.pow_addRight
added theorem Equiv.pow_mulLeft
added theorem Equiv.pow_mulRight
added theorem Equiv.zpow_addLeft
added theorem Equiv.zpow_addRight
added theorem Equiv.zpow_mulLeft
added theorem Equiv.zpow_mulRight