cast_comm — Mathlib

English

In a division ring, rational numbers embedded into the ring commute with every element. Equivalently, for every r in Q and a in α, (r : α) · a = a · (r : α).

Русский

В делении кольца рациональные числа, помещённые в кольцо, коммутируют с любым элементом. То есть для каждого r ∈ ℚ и a ∈ α выполняется (r : α) · a = a · (r : α).

LaTeX

$$$\forall r \in \mathbb{Q}, \forall a \in \alpha, \ (r : \alpha) \cdot a = a \cdot (r : \alpha).$$$

Lean4

theorem cast_comm (r : ℚ) (a : α) : (r : α) * a = a * r :=
  (cast_commute r a).eq

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