Mathlib Changelog
v3
Changelog
About
Github
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