Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_aut.conj_inv_apply

Modification history

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_inv_applyView on Github →