Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-06 13:16 730513c7

View on Github →

feat(group_theory/perm/basic): mul_left is a monoid hom (#17900) equiv.mul_left is a monoid homomorphism.

Estimated changes

deleted theorem equiv.perm.coe_pow
added theorem equiv.add_left_add
added theorem equiv.add_left_zero
added theorem equiv.add_right_add
added theorem equiv.add_right_zero
added theorem equiv.inv_add_left
added theorem equiv.inv_add_right
added theorem equiv.inv_mul_left
added theorem equiv.inv_mul_right
added theorem equiv.mul_left_mul
added theorem equiv.mul_left_one
added theorem equiv.mul_right_mul
added theorem equiv.mul_right_one
modified theorem equiv.perm.coe_mul
modified theorem equiv.perm.coe_one
added theorem equiv.perm.coe_pow
added theorem equiv.pow_add_left
added theorem equiv.pow_add_right
added theorem equiv.pow_mul_left
added theorem equiv.pow_mul_right
added theorem equiv.zpow_add_left
added theorem equiv.zpow_add_right
added theorem equiv.zpow_mul_left
added theorem equiv.zpow_mul_right