English
For q ∈ ℚ≥0 and r ∈ ℝ, ofReal(q • r) = q • r.
Русский
Для q ∈ ℚ≥0 и r ∈ ℝ верно: ofReal(q • r) = q • r.
LaTeX
$$$$\operatorname{ofReal}(q \cdot r) = q \cdot r.$$$$
Lean4
noncomputable instance instField : Field ℂ
where
mul_inv_cancel := @Complex.mul_inv_cancel
inv_zero := Complex.inv_zero
nnqsmul := (· • ·)
qsmul := (· • ·)
nnratCast_def q := by ext <;> simp [NNRat.cast_def, div_re, div_im, mul_div_mul_comm]
ratCast_def q := by ext <;> simp [Rat.cast_def, div_re, div_im, mul_div_mul_comm]
nnqsmul_def n z := Complex.ext_iff.2 <| by simp [NNRat.smul_def, smul_re, smul_im]
qsmul_def n z := Complex.ext_iff.2 <| by simp [Rat.smul_def, smul_re, smul_im]
