cast_commute — Mathlib

English

The integer cast commutes with every element of α: for all n ∈ ℤ and a ∈ α, n·a = a·n.

Русский

Приведение целого числа commutes с любым элементом алгебраической структуры: для всех n ∈ ℤ и a ∈ α, n·a = a·n.

LaTeX

$$$\forall (n : \mathbb{Z}) (a : \alpha), n^{\text{cast}} a = a n^{\text{cast}}$$$

Lean4

theorem cast_commute : ∀ (n : ℤ) (a : α), Commute (↑n) a
  | (n : ℕ), x => by simpa using n.cast_commute x
  | -[n+1], x => by
    simpa only [cast_negSucc, Commute.neg_left_iff, Commute.neg_right_iff] using (n + 1).cast_commute (-x)

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