Commit 2026-05-06 09:43 968bc313

View on Github →

chore(CategoryTheory/EpiMono): use to_dual (#38173) Generate declarations about Mono, SplitMono and SplitMonoCategory from the epic versions.

Estimated changes

Modified Mathlib/CategoryTheory/EpiMono.lean

deleted theorem CategoryTheory.IsIso.of_mono_retraction'

deleted theorem CategoryTheory.IsIso.of_mono_retraction

deleted theorem CategoryTheory.IsSplitMono.id

deleted theorem CategoryTheory.IsSplitMono.mk'

deleted def CategoryTheory.SplitMono.comp

deleted def CategoryTheory.SplitMono.map

deleted theorem CategoryTheory.SplitMono.mono

deleted def CategoryTheory.SplitMono.op

deleted def CategoryTheory.SplitMono.splitEpi

deleted theorem CategoryTheory.isIso_of_epi_of_isSplitMono

deleted theorem CategoryTheory.isSplitMono_of_mono

deleted theorem CategoryTheory.mono_comp_iff_of_isIso

deleted theorem CategoryTheory.mono_comp_iff_of_mono

deleted theorem CategoryTheory.op_mono_iff

deleted theorem CategoryTheory.unop_mono_iff

Modified Mathlib/Tactic/Translate/ToDual.lean