Documentation Verification Report

Fractions

📁 Source: Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean

Statistics

Metric	Count
Definitions `LeftFraction₂`, `Y'`, `f`, `f'`, `fst`, `s`, `snd`, `LeftFraction₂Rel`, `LeftFraction₃`, `Y'`, `f`, `f'`, `f''`, `forgetFst`, `forgetSnd`, `forgetThd`, `fst`, `s`, `snd`, `thd`, `RightFraction₂`, `X'`, `f`, `f'`, `fst`, `s`, `snd`	27
Theorems `exists_leftFraction₂`, `exists_leftFraction₃`, `hs`, `map_eq_iff`, `fst`, `snd`, `hs`, `exists_leftFraction₂`, `hs`	9
Total	36

CategoryTheory.Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_leftFraction₂` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.map` `CategoryTheory.MorphismProperty.LeftFraction₂.fst` `inverts` `CategoryTheory.MorphismProperty.LeftFraction₂.snd`	—	`inverts` `exists_leftFraction` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative` `CategoryTheory.Functor.map_comp` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.cancel_mono` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc`
`exists_leftFraction₃` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.map` `CategoryTheory.MorphismProperty.LeftFraction₃.fst` `inverts` `CategoryTheory.MorphismProperty.LeftFraction₃.snd` `CategoryTheory.MorphismProperty.LeftFraction₃.thd`	—	`inverts` `exists_leftFraction₂` `exists_leftFraction` `CategoryTheory.MorphismProperty.LeftFraction₂.hs` `CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.Functor.map_comp` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.cancel_mono` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc`

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`LeftFraction₂` 📖	CompData	—
`LeftFraction₂Rel` 📖	MathDef	1 math math: `LeftFraction₂.map_eq_iff`
`LeftFraction₃` 📖	CompData	—
`RightFraction₂` 📖	CompData	—

CategoryTheory.MorphismProperty.LeftFraction₂

Definitions

Name	Category	Theorems
`Y'` 📖	CompOp	2 math math: `hs`, `CategoryTheory.MorphismProperty.RightFraction₂.exists_leftFraction₂`
`f` 📖	CompOp	1 math math: `CategoryTheory.MorphismProperty.RightFraction₂.exists_leftFraction₂`
`f'` 📖	CompOp	1 math math: `CategoryTheory.MorphismProperty.RightFraction₂.exists_leftFraction₂`
`fst` 📖	CompOp	4 math math: `map_add`, `map_eq_iff`, `CategoryTheory.Localization.exists_leftFraction₂`, `CategoryTheory.MorphismProperty.LeftFraction₂Rel.fst`
`s` 📖	CompOp	2 math math: `hs`, `CategoryTheory.MorphismProperty.RightFraction₂.exists_leftFraction₂`
`snd` 📖	CompOp	4 math math: `map_add`, `CategoryTheory.MorphismProperty.LeftFraction₂Rel.snd`, `map_eq_iff`, `CategoryTheory.Localization.exists_leftFraction₂`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hs` 📖	mathematical	—	`Y'` `s`	—	—
`map_eq_iff` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.map` `fst` `CategoryTheory.Localization.inverts` `snd` `CategoryTheory.MorphismProperty.LeftFraction₂Rel`	—	`CategoryTheory.Localization.inverts` `CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff` `CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext` `hs` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.MorphismProperty.LeftFraction₂Rel.fst` `CategoryTheory.MorphismProperty.LeftFraction₂Rel.snd`

CategoryTheory.MorphismProperty.LeftFraction₂Rel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst` 📖	mathematical	`CategoryTheory.MorphismProperty.LeftFraction₂Rel`	`CategoryTheory.MorphismProperty.LeftFractionRel` `CategoryTheory.MorphismProperty.LeftFraction₂.fst`	—	—
`snd` 📖	mathematical	`CategoryTheory.MorphismProperty.LeftFraction₂Rel`	`CategoryTheory.MorphismProperty.LeftFractionRel` `CategoryTheory.MorphismProperty.LeftFraction₂.snd`	—	—

CategoryTheory.MorphismProperty.LeftFraction₃

Definitions

Name	Category	Theorems
`Y'` 📖	CompOp	1 math math: `hs`
`f` 📖	CompOp	—
`f'` 📖	CompOp	—
`f''` 📖	CompOp	—
`forgetFst` 📖	CompOp	—
`forgetSnd` 📖	CompOp	—
`forgetThd` 📖	CompOp	—
`fst` 📖	CompOp	1 math math: `CategoryTheory.Localization.exists_leftFraction₃`
`s` 📖	CompOp	1 math math: `hs`
`snd` 📖	CompOp	1 math math: `CategoryTheory.Localization.exists_leftFraction₃`
`thd` 📖	CompOp	1 math math: `CategoryTheory.Localization.exists_leftFraction₃`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hs` 📖	mathematical	—	`Y'` `s`	—	—

CategoryTheory.MorphismProperty.RightFraction₂

Definitions

Name	Category	Theorems
`X'` 📖	CompOp	2 math math: `hs`, `exists_leftFraction₂`
`f` 📖	CompOp	1 math math: `exists_leftFraction₂`
`f'` 📖	CompOp	1 math math: `exists_leftFraction₂`
`fst` 📖	CompOp	—
`s` 📖	CompOp	2 math math: `hs`, `exists_leftFraction₂`
`snd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_leftFraction₂` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X'` `CategoryTheory.MorphismProperty.LeftFraction₂.Y'` `f` `CategoryTheory.MorphismProperty.LeftFraction₂.s` `s` `CategoryTheory.MorphismProperty.LeftFraction₂.f` `f'` `CategoryTheory.MorphismProperty.LeftFraction₂.f'`	—	`CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'`
`hs` 📖	mathematical	—	`X'` `s`	—	—

---

← Back to Index