Module

FunctionField_exists_ratFuncAlgHom_apply_X_eq.lean

Nyll.AlgebraicCurves.FunctionFields.FunctionField_exists_ratFuncAlgHom_apply_X_eq

1 declaration indexed from sourceView source ↗

Module documentation

FunctionField exists ratFuncAlgHom apply X eq

A function outside the image of an algebraically closed base field defines an embedding of the rational function field that sends its variable to that function.

Imports5

Mathlib.FieldTheory.RatFunc.Basic
Mathlib.FieldTheory.RatFunc.AsPolynomial
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.FieldTheory.Minpoly.Basic
Mathlib.RingTheory.Algebraic.Basic

Imported by7

theorem

exists_ratFuncAlgHom_apply_X_eq

L32 ↗

AlgebraicCurve.FunctionField.exists_ratFuncAlgHom_apply_X_eq

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FunctionField_exists_ratFuncAlgHom_apply_X_eq
open Polynomial

Lean source · statement

theorem _root_.AlgebraicCurve.FunctionField.exists_ratFuncAlgHom_apply_X_eq {K F : Type*}
  [Field K] [IsAlgClosed K] [Field F] [Algebra K F] {g : F} (hg : g ∉ Set.range
  (algebraMap K F)) : ∃ φ : RatFunc K →ₐ[K] F, φ RatFunc.X = g

Module documentation

FunctionField exists ratFuncAlgHom apply X eq

Declarations

exists_ratFuncAlgHom_apply_X_eq