isReal_comp — Mathlib

English

If φ is a conjugation of σ, then φ ∘ algebraMap k K is real.

Русский

Если φ является сопряжением σ, то φ ∘ algebraMap k K является вещественным отображением.

LaTeX

$$IsReal(φ ∘ algebraMap k K)$$

Lean4

theorem isReal_comp (h : IsConj φ σ) : IsReal (φ.comp (algebraMap k K)) :=
  by
  ext1 x
  simp only [conjugate_coe_eq, RingHom.coe_comp, Function.comp_apply, ← h.eq, starRingEnd_apply, AlgEquiv.commutes]

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