Commit 2024-07-04 21:34 0b5b0644

View on Github →

chore: Move MulAction on Opposite, Pi, Prod, Sum, Sigma, Units (#13161) ... and add assert_not_exists MonoidWithZero everywhere.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/AddConstMap/Basic.lean

Modified Mathlib/Algebra/Algebra/NonUnitalHom.lean

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/BigOperators/Pi.lean

Created Mathlib/Algebra/Group/Action/Opposite.lean

added theorem MulOpposite.op_smul_eq_op_smul_op

added theorem MulOpposite.smul_eq_mul_unop

added theorem MulOpposite.unop_smul_eq_unop_smul_unop

added theorem op_smul_eq_mul

added theorem op_smul_mul

added theorem op_smul_op_smul

Renamed Mathlib/GroupTheory/GroupAction/Option.lean to Mathlib/Algebra/Group/Action/Option.lean

Created Mathlib/Algebra/Group/Action/Pi.lean

added theorem Function.extend_smul

added theorem Function.update_smul

added theorem Pi.faithfulSMul_at

added theorem Pi.smul_apply'

added theorem Set.piecewise_smul

Created Mathlib/Algebra/Group/Action/Prod.lean

added def MulAction.prodEquiv

added theorem Prod.pow_def

added theorem Prod.pow_fst

added theorem Prod.pow_mk

added theorem Prod.pow_snd

added theorem Prod.pow_swap

added theorem Prod.smul_def

added theorem Prod.smul_fst

added theorem Prod.smul_mk

added theorem Prod.smul_snd

added theorem Prod.smul_swap

added def smulMonoidHom

added def smulMulHom

Renamed Mathlib/GroupTheory/GroupAction/Sigma.lean to Mathlib/Algebra/Group/Action/Sigma.lean

Renamed Mathlib/GroupTheory/GroupAction/Sum.lean to Mathlib/Algebra/Group/Action/Sum.lean

Created Mathlib/Algebra/Group/Action/Units.lean

added theorem IsUnit.inv_smul

added theorem IsUnit.smul

added theorem Units.smul_def

added theorem Units.smul_inv

added theorem Units.smul_isUnit

added theorem Units.smul_mk_apply

added theorem Units.val_smul

Modified Mathlib/Algebra/Group/Aut.lean

Modified Mathlib/Algebra/Group/NatPowAssoc.lean

Modified Mathlib/Algebra/Group/PNatPowAssoc.lean

Modified Mathlib/Algebra/GroupPower/IterateHom.lean

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

Modified Mathlib/Algebra/Module/Basic.lean

Modified Mathlib/Algebra/Module/PointwisePi.lean

Modified Mathlib/Algebra/Order/CauSeq/Basic.lean

Modified Mathlib/Algebra/Order/Floor/Div.lean

Modified Mathlib/Algebra/Ring/CentroidHom.lean

Modified Mathlib/Algebra/SMulWithZero.lean

Modified Mathlib/Algebra/Star/Basic.lean

Modified Mathlib/Algebra/Star/Prod.lean

Modified Mathlib/Data/Finset/Pointwise.lean

Modified Mathlib/GroupTheory/GroupAction/Embedding.lean

Modified Mathlib/GroupTheory/GroupAction/Opposite.lean

deleted theorem MulOpposite.op_smul_eq_op_smul_op

deleted theorem MulOpposite.smul_eq_mul_unop

deleted theorem MulOpposite.unop_smul_eq_unop_smul_unop

deleted theorem op_smul_eq_mul

deleted theorem op_smul_mul

deleted theorem op_smul_op_smul

Modified Mathlib/GroupTheory/GroupAction/Pi.lean

deleted theorem Function.extend_smul

deleted theorem Function.update_smul

deleted theorem Pi.faithfulSMul_at

deleted theorem Pi.smul_apply'

deleted theorem Set.piecewise_smul

Modified Mathlib/GroupTheory/GroupAction/Prod.lean

deleted def MulAction.prodEquiv

deleted theorem Prod.pow_def

deleted theorem Prod.pow_fst

deleted theorem Prod.pow_mk

deleted theorem Prod.pow_snd

deleted theorem Prod.pow_swap

deleted theorem Prod.smul_def

deleted theorem Prod.smul_fst

deleted theorem Prod.smul_mk

deleted theorem Prod.smul_snd

deleted theorem Prod.smul_swap

deleted def smulMonoidHom

deleted def smulMulHom

Modified Mathlib/GroupTheory/GroupAction/Units.lean

deleted theorem IsUnit.inv_smul

deleted theorem IsUnit.smul

deleted theorem Units.smul_def

deleted theorem Units.smul_inv

deleted theorem Units.smul_isUnit

deleted theorem Units.smul_mk_apply

deleted theorem Units.val_smul

Modified Mathlib/RepresentationTheory/Action/Concrete.lean