equivalenceRightFractionRel — Mathlib

English

RightFractionRel defines an equivalence relation on W.RightFraction X Y; i.e., the relation is reflexive, symmetric, and transitive.

Русский

RightFractionRel задаёт эквивалентность на W.RightFraction X Y: рефлексивность, симметричность и транзитивность.

LaTeX

$$$Equivalence(W.RightFraction X Y, RightFractionRel)$$$

Lean4

theorem equivalenceRightFractionRel (X Y : C) [HasRightCalculusOfFractions W] :
    @_root_.Equivalence (W.RightFraction X Y) RightFractionRel
    where
  refl := RightFractionRel.refl
  symm := RightFractionRel.symm
  trans := RightFractionRel.trans

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