Commit 2022-12-06 09:09 bc3ae97e

View on Github →

feat: port group_theory.group_action.defs (#854) Tracking mathlib commit: dad7ecf9a1feae63e6e49f07619b7087403fb8d4

Estimated changes

added theorem AddMonoid.End.smul_def
added theorem Commute.smul_left
added theorem Commute.smul_right
added theorem Function.End.smul_def
added def MulAction.toFun
added theorem MulAction.toFun_apply
added def SMul.comp.smul
added def SMul.comp
added theorem SMulCommClass.symm
added theorem comp_smul_left
added theorem ite_smul
added theorem mul_smul_comm
added theorem mul_smul_one
added theorem ofAdd_smul
added theorem ofMul_vadd
added theorem one_smul
added theorem one_smul_eq_id
added def smulOneHom
added theorem smul_add
added theorem smul_assoc
added theorem smul_div'
added theorem smul_eq_mul
added theorem smul_inv'
added theorem smul_ite
added theorem smul_left_injective'
added theorem smul_mul'
added theorem smul_mul_assoc
added theorem smul_mul_smul
added theorem smul_neg
added theorem smul_one_mul
added theorem smul_one_smul
added theorem smul_smul
added theorem smul_smul_smul_comm
added theorem smul_sub
added theorem smul_zero
added theorem toAdd_vadd
added theorem toMul_smul