cast_mul — Mathlib

English

For all m,n in ZNum and any α with a non-associative ring structure, the embedding preserves multiplication: the image of m n equals the product of the images.

Русский

Для любых m,n ∈ ZNum и любой кольцевой структуры α сохраняется произведение: образ m n равен произведению образов.

LaTeX

$$$$\forall m,n \in ZNum,\ ((m * n : ZNum) : α) = (m : α) \cdot (n : α).$$$$

Lean4

theorem cast_mul [NonAssocRing α] (m n) : ((m * n : ZNum) : α) = m * n := by
  rw [← cast_to_int, mul_to_int, Int.cast_mul, cast_to_int, cast_to_int]

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