ModuleFinitelyGeneratedModel.lean
Nyll.GaloisCohomology.FieldTheory.FinitelyGeneratedModel
3 declarations indexed from sourceView source ↗ Module documentation
Affine integral models of finitely generated fields
Imports9
- Mathlib.RingTheory.Localization.FractionRing
- Mathlib.RingTheory.FiniteType
- Mathlib.Algebra.Algebra.Subalgebra.Lattice
- Mathlib.Algebra.Field.Subfield.Basic
- Mathlib.RingTheory.Jacobson.Ring
- Mathlib.Algebra.CharP.Basic
- Mathlib.RingTheory.DedekindDomain.Basic
- Mathlib.Algebra.Ring.Int.Units
- Lean.Elab.Tactic.Omega
Imported by3
Declarations
FieldTheory.exists_finiteType_int_model
DocumentationA finitely generated field is the fraction field of a finitely generated algebra over the integers.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FieldTheory
universe u
FieldTheory.int_isJacobsonRing
DocumentationThe integers form a Jacobson ring.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FieldTheory
universe u
FieldTheory.ringChar_ne_zero_of_finiteType_int
DocumentationA field that is finitely generated as a ring has positive characteristic.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FieldTheory
universe u