mul_assoc — Mathlib

English

Associativity of Holor multiplication: the two ways of multiplying three holors are equal up to a canonical homogeneous equality (HEq).

Русский

Сопряженность умножения Holor: две последовательности умножения трёх холоров совпадают до гомотопной эквивалентности (HEq).

LaTeX

$$$\mathrm{mul} (\mathrm{mul} x y) z \; \overset{HEq}{\cong} \; \mathrm{mul} x (\mathrm{mul} y z)$$$

Lean4

theorem mul_assoc [Semigroup α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃) :
    mul (mul x y) z ≍ mul x (mul y z) := by simp [cast_heq, mul_assoc0, assocLeft]

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