Commit 2023-07-05 04:52 d6a45165

View on Github →

feat: port Algebra.Category.Algebra.Basic (#4504)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/AlgebraCat/Basic.lean

added def AlgEquiv.toAlgebraIso

added def AlgebraCat.adj

added theorem AlgebraCat.coe_comp

added theorem AlgebraCat.coe_of

added def AlgebraCat.free

added theorem AlgebraCat.id_apply

added def AlgebraCat.of

added def AlgebraCat.ofHom

added theorem AlgebraCat.ofHom_apply

added def AlgebraCat.ofSelfIso

added structure AlgebraCat

added def CategoryTheory.Iso.toAlgEquiv

added def algEquivIsoAlgebraIso