Commit 2024-05-24 03:47 7476a96c

View on Github →

chore: Move MulAction to under Algebra (#13140) Move the content of GroupTheory.GroupAction.Defs that doesn't depend on GroupWithZero to a new file Algebra.Group.Action.Defs. This is part of #13027.

Estimated changes

added theorem Commute.smul_left
added theorem Commute.smul_right
added theorem Function.End.mul_def
added theorem Function.End.one_def
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 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 theorem smul_assoc
added theorem smul_div_assoc
added theorem smul_eq_mul
added theorem smul_left_injective'
added theorem smul_mul_assoc
added theorem smul_mul_smul
added theorem smul_one_mul
added theorem smul_one_smul
added theorem smul_pow
added theorem smul_smul
added theorem smul_smul_smul_comm
added theorem toAdd_vadd
added theorem toMul_smul
deleted def AddAction.toEndHom
deleted theorem Commute.smul_left
deleted theorem Commute.smul_right
deleted theorem Function.End.mul_def
deleted theorem Function.End.one_def
deleted theorem Function.End.smul_def
deleted def MulAction.compHom
deleted theorem MulAction.exists_smul_eq
deleted theorem MulAction.surjective_smul
deleted def MulAction.toEndHom
deleted def MulAction.toFun
deleted theorem MulAction.toFun_apply
deleted theorem SMul.comp.isScalarTower
deleted def SMul.comp.smul
deleted theorem SMul.comp.smulCommClass'
deleted theorem SMul.comp.smulCommClass
deleted def SMul.comp
deleted theorem SMulCommClass.symm
deleted theorem comp_smul_left
deleted theorem mul_smul_comm
deleted theorem mul_smul_one
deleted theorem ofAdd_smul
deleted theorem ofMul_vadd
deleted theorem one_smul
deleted theorem one_smul_eq_id
deleted theorem smul_assoc
deleted theorem smul_div_assoc
deleted theorem smul_eq_mul
deleted theorem smul_left_injective'
deleted theorem smul_mul_assoc
deleted theorem smul_mul_smul
deleted theorem smul_one_mul
deleted theorem smul_one_smul
deleted theorem smul_pow
deleted theorem smul_smul
deleted theorem smul_smul_smul_comm
deleted theorem toAdd_vadd
deleted theorem toMul_smul