Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-12 14:28 26e3eea8

View on Github →

feat(group_theory/group_action/defs): vadd_assoc_class (#15844) Additivize is_scalar_tower into a new class vadd_assoc_class.

Estimated changes

Modified src/algebra/group/to_additive.lean

Modified src/data/finset/pointwise.lean

Modified src/data/set/pointwise.lean

Modified src/group_theory/group_action/defs.lean

modified theorem has_smul.comp.is_scalar_tower

modified theorem smul_assoc

modified theorem smul_one_mul

modified theorem smul_one_smul

Modified src/order/filter/pointwise.lean