Commit 2022-12-21 05:22 e9bd329b

View on Github →

feat: port Algebra.Hom.Aut (#1111) d4f69d96f3532729da8ebb763f4bc26fcf640f06

Estimated changes

added theorem AddAut.apply_inv_self
added theorem AddAut.coe_mul
added theorem AddAut.coe_one
added def AddAut.conj
added theorem AddAut.conj_apply
added theorem AddAut.conj_inv_apply
added theorem AddAut.conj_symm_apply
added theorem AddAut.inv_apply_self
added theorem AddAut.inv_def
added theorem AddAut.mul_apply
added theorem AddAut.mul_def
added theorem AddAut.one_apply
added theorem AddAut.one_def
added def AddAut.toPerm
added theorem MulAut.apply_inv_self
added theorem MulAut.coe_mul
added theorem MulAut.coe_one
added def MulAut.conj
added theorem MulAut.conj_apply
added theorem MulAut.conj_inv_apply
added theorem MulAut.conj_symm_apply
added theorem MulAut.inv_apply_self
added theorem MulAut.inv_def
added theorem MulAut.mul_apply
added theorem MulAut.mul_def
added theorem MulAut.one_apply
added theorem MulAut.one_def
added def MulAut.toPerm
added def MulAut