Commit 2026-01-20 18:20 bbc2ce21

View on Github →

feat(RingTheory): field extension over perfect fields are smooth (#32617)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean

added theorem Algebra.finite_of_essFiniteType_of_isAlgebraic

added theorem IntermediateField.essFiniteType_iff

added theorem IntermediateField.fg_top

added theorem IntermediateField.fg_top_iff

deleted theorem IntermediateField.finite_of_fg_of_isAlgebraic

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean

Modified Mathlib/FieldTheory/SeparableClosure.lean

deleted theorem IntermediateField.FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure

added theorem IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure

Modified Mathlib/FieldTheory/SeparablyGenerated.lean

added theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType

deleted theorem exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_fg

Modified Mathlib/RingTheory/EssentialFiniteness.lean

added theorem Algebra.EssFiniteType.iff_of_algEquiv

added theorem Algebra.EssFiniteType.of_surjective

Created Mathlib/RingTheory/Smooth/Field.lean

added theorem Algebra.FormallySmooth.adjoin_of_algebraicIndependent

added theorem Algebra.FormallySmooth.of_algebraicIndependent

added theorem Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable