quot_mk_assoc_left — Mathlib

English

The left-associated products are congruent in the quotient: x*(y*z*w) equals x*(y*(z*w)) in the quotient.

Русский

Лева-ассоциированное произведение эквивалентно в фактор-множество: $x*(y*z*w)$ эквивалентно $x*(y*(z*w))$.

LaTeX

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

Lean4

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

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