English
There is a canonical ring isomorphism between any 𝕜 with RCLike structure and ℂ, given by φ(x) = Re(x) + Im(x)·i and φ^{-1}(z) = Re(z) + Im(z)·I.
Русский
Существует каноническое кольцо-изоморфизм между любым полем 𝕜 с структурой RCLike и ℂ, заданный формулой φ(x) = Re(x) + Im(x)·i и его обратной φ^{-1}(z) = Re(z) + Im(z)·I.
LaTeX
$$$\\\\exists φ: 𝕜 \\\\cong_{ring} \\\\mathbb{C}, \\\\phi(x) = \\\\operatorname{Re}x + \\\\operatorname{Im}x \\\\cdot i$$$
Lean4
/-- The natural isomorphism between `𝕜` satisfying `RCLike 𝕜` and `ℂ` when
`RCLike.im RCLike.I = 1`. -/
@[simps]
def _root_.RCLike.complexRingEquiv {𝕜 : Type*} [RCLike 𝕜] (h : RCLike.im (RCLike.I : 𝕜) = 1) : 𝕜 ≃+* ℂ
where
toFun x := RCLike.re x + RCLike.im x * I
invFun x := re x + im x * RCLike.I
left_inv x := by simp
right_inv x := by simp [h]
map_add' x y := by simp only [map_add, ofReal_add]; ring
map_mul' x
y := by
simp only [RCLike.mul_re, ofReal_sub, ofReal_mul, RCLike.mul_im, ofReal_add]
ring_nf
rw [I_sq]
ring
