rightFraction_fac — Mathlib

English

For a right fraction φ, the relation φ.rightFraction.s ≫ φ.f = φ.rightFraction.f ≫ φ.s holds.

Русский

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

LaTeX

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

Lean4

@[reassoc]
theorem rightFraction_fac [W.HasRightCalculusOfFractions] {X Y : C} (φ : W.LeftFraction X Y) :
    φ.rightFraction.s ≫ φ.f = φ.rightFraction.f ≫ φ.s :=
  φ.exists_rightFraction.choose_spec

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