pmul_assoc — Mathlib

English

The operation pmul is associative: pmul(pmul(f1,f2), f3) = pmul(f1, pmul(f2,f3)).

Русский

Операция pmul ассоциативна: pmul(pmul(f1,f2), f3) = pmul(f1, pmul(f2,f3)).

LaTeX

$$$$ \text{pmul} ( \text{pmul}(f_1,f_2), f_3 ) = \text{pmul}(f_1, \text{pmul}(f_2,f_3)) $$$$

Lean4

theorem pmul_assoc [SemigroupWithZero R] (f₁ f₂ f₃ : ArithmeticFunction R) :
    pmul (pmul f₁ f₂) f₃ = pmul f₁ (pmul f₂ f₃) := by
  ext
  simp only [pmul_apply, mul_assoc]

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