Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-25 18:32 6a418050

View on Github →

chore(group_theory/group_action/basic): to_additive attributes throughout (#8814)

Estimated changes

Modified src/group_theory/group_action/basic.lean

added theorem add_action.exists_vadd_eq

deleted theorem exists_smul_eq

added theorem mul_action.exists_smul_eq

modified theorem mul_action.fixed_eq_Inter_fixed_by

modified theorem mul_action.injective_of_quotient_stabilizer

modified theorem mul_action.mem_fixed_by

modified theorem mul_action.mem_fixed_points'

modified theorem mul_action.mem_fixed_points

modified theorem mul_action.mem_fixed_points_iff_card_orbit_eq_one

modified theorem mul_action.mem_orbit

modified theorem mul_action.mem_orbit_iff

modified theorem mul_action.mem_orbit_self

modified theorem mul_action.mem_orbit_smul

modified theorem mul_action.mem_stabilizer_iff

modified theorem mul_action.mem_stabilizer_submonoid_iff

modified theorem mul_action.of_quotient_stabilizer_mem_orbit

modified theorem mul_action.of_quotient_stabilizer_mk

modified theorem mul_action.of_quotient_stabilizer_smul

modified theorem mul_action.orbit_eq_iff

modified theorem mul_action.orbit_equiv_quotient_stabilizer_symm_apply

modified theorem mul_action.quotient.smul_coe

modified theorem mul_action.quotient.smul_mk

modified theorem mul_action.smul_mem_orbit_smul

modified theorem mul_action.stabilizer_quotient