nmul_assoc — Mathlib

English

Natural product is associative: a ⊗ b ⊗ c = a ⊗ (b ⊗ c).

Русский

Умножение по природе ассоциативно: a ⊗ b ⊗ c = a ⊗ (b ⊗ c).

LaTeX

$$$(a \otimes b) \otimes c = a \otimes (b \otimes c)$$$

Lean4

theorem nmul_assoc (a b c : Ordinal) : a ⨳ b ⨳ c = a ⨳ (b ⨳ c) :=
  by
  apply le_antisymm
  · rw [nmul_le_iff₃]
    intro a' ha b' hb c' hc
    repeat rw [nmul_assoc]
    exact nmul_nadd_lt₃' ha hb hc
  · rw [nmul_le_iff₃']
    intro a' ha b' hb c' hc
    repeat rw [← nmul_assoc]
    exact nmul_nadd_lt₃ ha hb hc
termination_by (a, b, c)

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