Emb — Mathlib

English

Field.Emb F E is the type of F-algebra homomorphisms from E to the algebraic closure of E.

Русский

Field.Emb F E — множество гомоморфизмов F-алгебр из E в алгебраическое замыкание E.

LaTeX

$$$\\text{Emb } F E := E \\to_{F} \\mathrm{AlgebraicClosure}(E)$$$

Lean4

/-- `Field.Emb F E` is the type of `F`-algebra homomorphisms from `E` to the algebraic closure
of `E`. -/
abbrev Emb :=
  E →ₐ[F] AlgebraicClosure E

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