cast_commute — Mathlib

English

For any α with a NonAssocSemiring structure, and n ∈ ℕ, (n : α) commutes with x ∈ α.

Русский

Для любого α с неассоциативной структурой полусистемы число n якобы коммутирует с элементом x.

LaTeX

$$$$ (n : \alpha) \cdot x = x \cdot (n : \alpha) $$$$

Lean4

theorem cast_commute (n : ℕ) (x : α) : Commute (n : α) x := by
  induction n with
  | zero => rw [Nat.cast_zero]; exact Commute.zero_left x
  | succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)

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