NYLL
Module

RationalFunctionField_nonempty_place_of_ratFunc_tower.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_nonempty_place_of_ratFunc_tower
1 declaration indexed from sourceView source ↗

Module documentation

Rational Function Field nonempty place of rat Func tower

Imports3
Imported by4

Declarations

theorem

nonempty_place_of_ratFunc_tower

L27 ↗
AlgebraicCurve.RationalFunctionField.nonempty_place_of_ratFunc_tower
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFieldPlaceRatFuncTower
open AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.nonempty_place_of_ratFunc_tower (K : Type*)
  [Field K]
    (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
    [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable
      (RatFunc K) F] :
    Nonempty (AlgebraicCurve.Place K F)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.