Mathlib Changelog
v4
Changelog
About
Github
Commit
2022-12-21 05:22
e9bd329b
View on Github →
feat: port Algebra.Hom.Aut (
#1111
) d4f69d96f3532729da8ebb763f4bc26fcf640f06
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Algebra/Hom/Aut.lean
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