Theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mk

Modification history

2025-07-25 22:49
Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
chore: fix more indentation (#27494) …
Modified CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mkView on Github →
2024-08-01 02:49
Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
chore: backports for leanprover/lean4#4814 (part 8) (#15349) …
Modified CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mkView on Github →
2024-02-22 12:56
Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
feat(CategoryTheory/Localization): construction of a localized category using left fractions (#10606) …
Added CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mkView on Github →