Commit 2025-04-17 01:13 e3601d1f

View on Github →

chore: automatically additivize IsScalarTower (#24115)

Estimated changes

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

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

Modified Mathlib/Algebra/Group/Action/Pointwise/Finset.lean

Modified Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

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

Modified Mathlib/Algebra/Order/Group/Action/Synonym.lean

Modified Mathlib/Analysis/Normed/Lp/WithLp.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

modified theorem SMulMemClass.ofIsScalarTower

Modified Mathlib/Order/Filter/Pointwise.lean

Modified Mathlib/Tactic/ToAdditive/Frontend.lean

Modified Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean

Modified Mathlib/Topology/Algebra/UniformMulAction.lean