quot_mk_assoc — Mathlib

English

The quotient map respects associativity: the quotient of x*y*z equals the quotient of x*(y*z).

Русский

Квази-отношение сохраняет ассоциативность: образ по отношению к $x*y*z$ равен образу к $x*(y*z)$.

LaTeX

$$$\\operatorname{Quot.mk}(\\operatorname{AssocRel}(\\alpha))(x \\ast y \\ast z) = \\operatorname{Quot.mk}(\\operatorname{AssocRel}(\\alpha))(x \\ast (y \\ast z))$$$

Lean4

@[to_additive]
theorem quot_mk_assoc (x y z : α) : Quot.mk (AssocRel α) (x * y * z) = Quot.mk _ (x * (y * z)) :=
  Quot.sound (AssocRel.intro _ _ _)

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