isReal_comp_iff — Mathlib

English

Let φ: K → ℂ be a homomorphism and f: k ≃+* K a Galois automorphism; then IsReal(φ ∘ f) holds if and only if IsReal(φ) holds, i.e. Real-ness is preserved under Galois conjugation.

Русский

Пусть φ: K → ℂ — гомоморфизм, a f: k ≃+* K — галуа-автоморфизм; тогда φ ∘ f реален тогда и только тогда, когда φ реален; т.е. реальность сохраняется при гало-замещении.

LaTeX

$$$\operatorname{IsReal}(φ \circ f) \iff \operatorname{IsReal}(φ) \quad (\text{при } IsGalois(k,K))$$$

Lean4

theorem isReal_comp_iff {f : k ≃+* K} {φ : K →+* ℂ} : IsReal (φ.comp (f : k →+* K)) ↔ IsReal φ :=
  ⟨fun H ↦ by convert H.comp f.symm.toRingHom; ext1; simp, IsReal.comp _⟩

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