Commit 2024-07-16 22:43 5eae12e5

View on Github →

chore: Move group lemmas out of GroupTheory.GroupAction.Group (#14705) The rest of the file is now purely about GroupWithZero and alike, and will be moved under Algebra.GroupWithZero.Action in a future PR.

Estimated changes

added def MulAction.toPerm
added def arrowAction
added theorem invOf_smul_eq_iff
added theorem invOf_smul_smul
added theorem isUnit_smul_iff
added theorem smul_invOf_smul
added theorem smul_left_cancel
added theorem smul_left_cancel_iff
deleted def AddAction.toPermHom
deleted theorem IsUnit.smul_left_cancel
deleted def MulAction.toPerm
deleted def MulAction.toPermHom
deleted def arrowAction
deleted theorem invOf_smul_eq_iff
deleted theorem invOf_smul_smul
deleted theorem isUnit_smul_iff
deleted theorem smul_eq_iff_eq_invOf_smul
deleted theorem smul_eq_iff_eq_inv_smul
deleted theorem smul_invOf_smul
deleted theorem smul_left_cancel
deleted theorem smul_left_cancel_iff