coe_real_complex_mul — Mathlib

English

For r ∈ ℝ and z ∈ ℂ, the real scalar action agrees with quaternion multiplication: (r • z : ℍ) = ↑r · ↑z.

Русский

Для r ∈ ℝ и z ∈ ℂ, действие скаляра над ℍ согласуется с умножением в кватернионах: (r • z : ℍ) = ↑r · ↑z.

LaTeX

$$$ (r \\cdot z)_{\\mathbb{H}} = r \\cdot \\hat{z} \\quad (r ∈ \\mathbb{R}, z ∈ \\mathbb{C}).$$$

Lean4

@[simp, norm_cast]
theorem coe_real_complex_mul (r : ℝ) (z : ℂ) : (r • z : ℍ) = ↑r * ↑z := by ext <;> simp

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