comp — Mathlib

English

If φ: K → ℂ is real and f: k → K is a field isomorphism (over k), then the composite φ ∘ f: k → ℂ is real as well.

Русский

Если φ: K → ℂ реализовано реальным образом и f: k → K — изоморфизм полей (над k), то композиция φ ∘ f: k → ℂ также является реальным отображением.

LaTeX

$$$\operatorname{IsReal}(φ \circ f) \quad\text{given } φ \text{ real and } f: k \to K\text{ a isomorphism}$$$

Lean4

theorem comp (f : k →+* K) {φ : K →+* ℂ} (hφ : IsReal φ) : IsReal (φ.comp f) := by ext1 x;
  simpa using RingHom.congr_fun hφ (f x)

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