mul_comm — Mathlib

English

Nimber multiplication is commutative: a*b = b*a.

Русский

Умножение Nimber коммутативно: a*b = b*a.

LaTeX

$$$ a \cdot b = b \cdot a $$$

Lean4

protected theorem mul_comm (a b : Nimber) : a * b = b * a :=
  by
  apply le_antisymm <;> refine mul_le_of_forall_ne fun x hx y hy ↦ ?_
  on_goal 1 => rw [add_comm (x * _), Nimber.mul_comm a, Nimber.mul_comm x, Nimber.mul_comm x]
  on_goal 2 => rw [add_comm (x * _), ← Nimber.mul_comm y, ← Nimber.mul_comm a, ← Nimber.mul_comm y]
  all_goals exact mul_ne_of_lt y hy x hx
termination_by (a, b)

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