Commit 2025-02-19 17:41 2bfb92f1

View on Github →

chore(Algebra/Group/Action): group similar lemmas (#21028) Swap imports and move lemmas between pairs of files to avoid scattering families of lemmas. Make the concrete action by Function.End depend on generic properties FaithfulSMul/IsPretransitive rather than the other way around.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/AddConstMap/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

Modified Mathlib/Algebra/GradedMonoid.lean

Modified Mathlib/Algebra/Group/Action/Defs.lean

added theorem MulOpposite.smul_eq_mul_unop

added theorem op_smul_eq_mul

modified theorem smul_eq_mul

Modified Mathlib/Algebra/Group/Action/End.lean

added def AddAction.toEndHom

deleted def MonoidHom.smulOneHom

deleted theorem MulAction.compHom_smul_def

deleted def monoidHomEquivMulActionIsScalarTower

Modified Mathlib/Algebra/Group/Action/Faithful.lean

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

added def MonoidHom.smulOneHom

added theorem MulAction.IsPretransitive.of_compHom

added theorem MulAction.compHom_smul_def

added theorem MulAction.isPretransitive_compHom

added def monoidHomEquivMulActionIsScalarTower

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

deleted theorem MulOpposite.smul_eq_mul_unop

deleted theorem op_smul_eq_mul

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

Modified Mathlib/Algebra/Group/Action/Pretransitive.lean

deleted theorem MulAction.IsPretransitive.of_compHom

deleted theorem MulAction.isPretransitive_compHom

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

Modified Mathlib/Algebra/Group/Action/Sigma.lean

Modified Mathlib/Algebra/Group/Action/TypeTags.lean

deleted def AddAction.toEndHom

Modified Mathlib/Algebra/GroupWithZero/Action/End.lean

Modified Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean

modified theorem Finset.inv_op_smul_finset_distrib₀

Modified Mathlib/Algebra/Module/Defs.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

Modified Mathlib/GroupTheory/Perm/Basic.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Quotient.lean

Modified Mathlib/MeasureTheory/Integral/Asymptotics.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean