Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-06 15:46 5773bc63

View on Github →

feat(group_theory/group_action/conj_act): conjugation action of groups (#8627)

Estimated changes

Modified src/data/equiv/mul_add_aut.lean

Created src/group_theory/group_action/conj_act.lean

added theorem conj_act.card

added theorem conj_act.fixed_points_eq_center

added def conj_act.of_conj_act

added theorem conj_act.of_conj_act_inv

added theorem conj_act.of_conj_act_mul

added theorem conj_act.of_conj_act_one

added theorem conj_act.of_conj_act_to_conj_act

added theorem conj_act.of_conj_act_zero

added theorem conj_act.of_mul_symm_eq

added theorem conj_act.smul_def

added theorem conj_act.smul_eq_mul_aut_conj

added def conj_act.to_conj_act

added theorem conj_act.to_conj_act_inv

added theorem conj_act.to_conj_act_mul

added theorem conj_act.to_conj_act_of_conj_act

added theorem conj_act.to_conj_act_one

added theorem conj_act.to_conj_act_zero

added theorem conj_act.to_mul_symm_eq

added theorem conj_act.«forall»

added def conj_act