Def Algebra.of

Modification history

2021-07-09 15:19

src/algebra/category/Algebra/basic.lean

feat(algebra/category): provide right adjoint instances for forget (#8235) …

Modified Algebra.of View on Github →

2020-09-01 12:18

src/algebra/category/Algebra/basic.lean

refactor(algebra/category/*, category_theory/concrete_category): generalize universes for concrete categories (#3687) …

Modified Algebra.of View on Github →

2020-06-17 11:06

src/algebra/category/Algebra/basic.lean

feat(algebra/category/Algebra): basic setup for category of bundled R-algebras (#3047) …

Added Algebra.of View on Github →