realRingEquiv — Mathlib

English

There is a ring isomorphism K ≃+* ℝ when I = 0, given by the real part.

Русский

При условии I = 0 существует кольцевое изоморфизм K ≃+* ℝ, задаваемый вещественной частью.

LaTeX

$$$$ realRingEquiv (h : I = 0) : K \\simeq_+* \\mathbb{R}. $$$$

Lean4

/-- The natural isomorphism between `𝕜` satisfying `RCLike 𝕜` and `ℝ` when `RCLike.I = 0`. -/
@[simps]
def realRingEquiv (h : I = (0 : K)) : K ≃+* ℝ where
  toFun := re
  invFun := (↑)
  left_inv x := by nth_rw 2 [← re_add_im x]; simp [h]
  right_inv := ofReal_re
  map_add' := map_add re
  map_mul' := by simp [im_eq_zero h]

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