Theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux

Modification history

2024-07-27 07:35

Mathlib/CategoryTheory/Limits/MonoCoprod.lean

chore: robustifying for debug.byAsSorry (part 8) (#15149) …

Modified CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux View on Github →

2024-02-12 10:30

Mathlib/CategoryTheory/Limits/MonoCoprod.lean

feat(CategoryTheory/Limits/MonoCoprod): inclusions of subcoproducts are mono (#10400) …

Added CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux View on Github →