ModuleTranscendence.lean
Nyll.SchemeTheory.Pi1.FunctionFields.Transcendence
3 declarations indexed from sourceView source ↗ Module documentation
Finite generation of fraction fields
Finite algebra generation gives finite field generation, and algebraic finitely generated field extensions are finite. The file also records smoothness of polynomial fraction fields.
Imports3
- Mathlib.Algebra.Lie.OfAssociative
- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
- Mathlib.RingTheory.Smooth.Basic
Imported by1
Declarations
Algebra.finite_of_intermediateFieldFG_of_isAlgebraic
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u
variable (k K : Type u) [Field k] [Field K] [Algebra k K]
Algebra.formallySmooth_fractionRing_mvPolynomial
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u
variable (k K : Type u) [Field k] [Field K] [Algebra k K]
Algebra.FiniteType.FG_top_of_isFractionRing
DocumentationIf S is of finite type over R and K the fraction field of S, then K is finitely generated over R as a field.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u
variable (k K : Type u) [Field k] [Field K] [Algebra k K]