Module

FiniteAlgebraicConstants.lean

Nyll.GaloisCohomology.FieldTheory.FiniteAlgebraicConstants

2 declarations indexed from sourceView source ↗

Module documentation

Finiteness of algebraic constants in a finitely generated field

Imports6

Mathlib.RingTheory.AlgebraicIndependent.Adjoin
Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Mathlib.RingTheory.Algebraic.Integral
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.LinearAlgebra.FiniteDimensional.Basic

Imported by4

theorem

finite_algebraic_subextension

L24 ↗

FieldTheory.finite_algebraic_subextension

Documentation

An algebraic subextension of a finitely generated field extension is finite.

Source context 3 commands

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

namespace FieldTheory
universe u v w
attribute [local instance] MvPolynomial.algebraMvPolynomial FractionRing.liftAlgebra

Lean source · statement

theorem finite_algebraic_subextension
    (F : Type u) (C : Type v) (K : Type w)
    [Field F] [Field C] [Field K] [Algebra F C] [Algebra F K] [Algebra C K]
    [IsScalarTower F C K] [Algebra.IsAlgebraic F C] [Algebra.EssFiniteType F K] :
    Module.Finite F C

theorem

finite_algebraicClosure_of_finite_base

L66 ↗

FieldTheory.finite_algebraicClosure_of_finite_base