Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_aut.conj_apply

Modification history

2021-10-26 17:54
src/data/equiv/mul_add_aut.lean
feat(group_theory/subgroup/basic): Define characteristic subgroups (#9921) …
Modified add_aut.conj_applyView on Github →
2021-03-29 13:12
src/data/equiv/mul_add_aut.lean
feat(data/equiv/mul_add_aut): adding conjugation in an additive group (#6774) …
Added add_aut.conj_applyView on Github →