Commit 2023-02-16 06:14 cf6e83b8

View on Github →

feat: port CategoryTheory.Endomorphism (#2310)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Endomorphism.lean

added theorem CategoryTheory.Aut.Aut_inv_def

added theorem CategoryTheory.Aut.Aut_mul_def

added def CategoryTheory.Aut.autMulEquivOfIso

added def CategoryTheory.Aut.unitsEndEquivAut

added def CategoryTheory.Aut

added def CategoryTheory.End.asHom

added theorem CategoryTheory.End.mul_def

added def CategoryTheory.End.of

added theorem CategoryTheory.End.one_def

added theorem CategoryTheory.End.smul_left

added theorem CategoryTheory.End.smul_right

added def CategoryTheory.End

added def CategoryTheory.Functor.mapAut

added def CategoryTheory.Functor.mapEnd

added theorem CategoryTheory.isUnit_iff_isIso