Extension — Mathlib

English

If φ is obtained as an extension of ψ with φ ∈ ComplexEmbedding.Extension L ψ, then φ.val ∘ algebraMap K L = ψ.

Русский

Если φ является расширением ψ через Extension L ψ, тогда φ.val ∘ algebraMap K L = ψ.

LaTeX

$$φ.val ∘ algebraMap K L = ψ$$

Lean4

/-- If `L/K` and `ψ : K →+* ℂ`, then the type of `ComplexEmbedding.Extension L ψ` consists of all
`φ : L →+* ℂ` such that `φ.comp (algebraMap K L) = ψ`. -/
protected abbrev Extension :=
  { φ : L →+* ℂ // φ.comp (algebraMap K L) = ψ }

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