Theorem CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'

Modification history

2024-08-02 06:24

Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean

chore: backports for leanprover/lean4#4814 (part 12) (#15396) …

Modified CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'View on Github →

2024-06-25 06:39

Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean

feat(CategoryTheory): constructor for right derivability structures (#12676) …

Added CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'View on Github →