Commit 2026-02-12 18:48 ab2f778f

View on Github →

chore(CategoryTheory/Subobject): missing simp lemma on self equalizers (#35177) Missing simp lemma on equalizerSubobject f f = ⊤.

Estimated changes

Modified Mathlib/CategoryTheory/Subobject/Limits.lean

added theorem CategoryTheory.Limits.equalizerSubobject_of_self

modified theorem CategoryTheory.Limits.kernelSubobject_zero