Commit 2025-02-05 17:02 d7a81bf7

View on Github →

refactor(Algebra/Category): clean up remaining uses of HasForget (#21460) This removes the remaining references to HasForget in the folder Mathlib/Algebra/Category, upgrading all instances to ConcreteCategory.

Estimated changes

Modified Mathlib/Algebra/Category/BialgebraCat/Basic.lean

Modified Mathlib/Algebra/Category/BoolRing.lean

Modified Mathlib/Algebra/Category/CoalgebraCat/Basic.lean

deleted def CoalgebraCat.of

Modified Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean

Modified Mathlib/Algebra/Category/FGModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/GrpWithZero.lean

added theorem GrpWithZero.hom_comp

added theorem GrpWithZero.hom_id

deleted def GrpWithZero.of

added structure GrpWithZero

deleted def GrpWithZero

Modified Mathlib/Algebra/Category/HopfAlgebraCat/Basic.lean

deleted def HopfAlgebraCat.of