Commit 2024-07-12 17:57 c0af29f6

View on Github →

chore: Move more lemmas to Algebra.Group.Action.Defs (#14677) Those will be needed in a future file Algebra.GroupWithZero.Action.Defs

Estimated changes

added theorem Commute.smul_left_iff
added theorem Commute.smul_right_iff
added theorem eq_inv_smul_iff
added theorem inv_smul_eq_iff
added theorem inv_smul_smul
added theorem smul_inv
added theorem smul_inv_smul
added theorem smul_zpow
deleted theorem Commute.smul_left_iff
deleted theorem Commute.smul_right_iff
deleted theorem eq_inv_smul_iff
deleted theorem inv_smul_eq_iff
deleted theorem inv_smul_smul
deleted theorem smul_inv
deleted theorem smul_inv_smul
deleted theorem smul_zpow