leftFraction_fac — Mathlib

English

For a left fraction φ, the relation φ.f ≫ φ.leftFraction.s = φ.s ≫ φ.leftFraction.f holds.

Русский

Для левой дроби φ выполняется равенство φ.f ≫ φ.leftFraction.s = φ.s ≫ φ.leftFraction.f.

LaTeX

$$φ.f \circ φ.leftFraction.s = φ.s \circ φ.leftFraction.f$$

Lean4

@[reassoc]
theorem leftFraction_fac [W.HasLeftCalculusOfFractions] {X Y : C} (φ : W.RightFraction X Y) :
    φ.f ≫ φ.leftFraction.s = φ.s ≫ φ.leftFraction.f :=
  φ.exists_leftFraction.choose_spec

Похожие утверждения