English
There is a noncomputable Real-Complex-Like structure on ℂ (RCLike ℂ).
Русский
На ℂ существует невычислимая структура RCLike (ℂ как RCLike).
LaTeX
$$$ \\text{RCLike}(\\\\mathbb{C}) $$$
Lean4
noncomputable instance : RCLike ℂ
where
re := ⟨⟨Complex.re, Complex.zero_re⟩, Complex.add_re⟩
im := ⟨⟨Complex.im, Complex.zero_im⟩, Complex.add_im⟩
I := Complex.I
I_re_ax := I_re
I_mul_I_ax := .inr Complex.I_mul_I
re_add_im_ax := re_add_im
ofReal_re_ax := ofReal_re
ofReal_im_ax := ofReal_im
mul_re_ax := mul_re
mul_im_ax := mul_im
conj_re_ax _ := rfl
conj_im_ax _ := rfl
conj_I_ax := conj_I
norm_sq_eq_def_ax z := (normSq_eq_norm_sq z).symm
mul_im_I_ax _ := mul_one _
toPartialOrder := Complex.partialOrder
le_iff_re_im := Iff.rfl
