Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-12 05:40 2efabeb7

View on Github →

feat(group_theory/group_action/defs): is_central_vadd (#17446) Define is_central_vadd, the additive version of is_central_scalar. Tag a few forgotten declarations with to_additive.

Estimated changes

Modified src/algebra/punit_instances.lean

modified theorem punit.smul_eq

Modified src/group_theory/group_action/defs.lean

Modified src/group_theory/group_action/opposite.lean

Modified src/group_theory/group_action/option.lean

Modified src/group_theory/group_action/pi.lean

Modified src/group_theory/group_action/prod.lean

Modified src/group_theory/group_action/sigma.lean

Modified src/group_theory/group_action/sum.lean

Modified src/order/filter/pointwise.lean

Modified src/tactic/to_additive.lean

Modified src/topology/algebra/const_mul_action.lean

Modified src/topology/algebra/mul_action.lean

Modified src/topology/algebra/uniform_mul_action.lean

modified theorem uniform_space.completion.smul_def