Module

Place_exists_ord_sub_algebraMap_pos_of_transcendental.lean

Nyll.AlgebraicCurves.Places.Place_exists_ord_sub_algebraMap_pos_of_transcendental

3 declarations indexed from sourceView source ↗

Module documentation

Place exists ord sub algebra Map pos of transcendental

Imports3

Imported by2

theorem

transcendental_sub_algebraMap

L30 ↗

AlgebraicCurves.Places.Proofs.Place_exists_ord_sub_algebraMap_pos_of_transcendental.POV.transcendental_sub_algebraMap

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_ord_sub_algebraMap_pos_of_transcendental
open AlgebraicCurve
open scoped IntermediateField
namespace POV

Lean source · statement

theorem transcendental_sub_algebraMap {K M : Type*} [Field K] [Field M] [Algebra K M] {t : M} (ht :
  Transcendental K t) (c : K) :
    Transcendental K (t - algebraMap K M c)

theorem

not_isUnit_of_transcendental

L39 ↗

AlgebraicCurves.Places.Proofs.Place_exists_ord_sub_algebraMap_pos_of_transcendental.POV.not_isUnit_of_transcendental

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_ord_sub_algebraMap_pos_of_transcendental
open AlgebraicCurve
open scoped IntermediateField
namespace POV

Lean source · statement

theorem not_isUnit_of_transcendental {K M : Type*} [Field K] [Field M] [Algebra K M] {f : M} (hf :
  Transcendental K f) :
    ¬ IsUnit (⟨f, Algebra.subset_adjoin (Set.mem_singleton f)⟩ : Algebra.adjoin K ({f} : Set M))

theorem

exists_ord_sub_algebraMap_pos_of_transcendental

L59 ↗

AlgebraicCurve.Place.exists_ord_sub_algebraMap_pos_of_transcendental

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_ord_sub_algebraMap_pos_of_transcendental
open AlgebraicCurve
open scoped IntermediateField
open POV in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.exists_ord_sub_algebraMap_pos_of_transcendental {K M : Type*}
  [Field K] [Field M] [Algebra K M] (t : M) (ht : Transcendental K t)
    [FiniteDimensional K⟮t⟯ M] [Algebra.IsSeparable K⟮t⟯ M] (c : K) :
    ∃ v : AlgebraicCurve.Place K M, 0 < v.ord (t - algebraMap K M c)

Module documentation

Place exists ord sub algebra Map pos of transcendental

Declarations

transcendental_sub_algebraMap

not_isUnit_of_transcendental

exists_ord_sub_algebraMap_pos_of_transcendental