Commit 2025-11-23 19:05 fb93b161

View on Github →

feat(FieldTheory): prerequisites for #31489 (#31875)

Estimated changes

Modified Mathlib/FieldTheory/IntermediateField/Algebraic.lean

added theorem IntermediateField.finrank_lt_of_gt

Modified Mathlib/FieldTheory/Normal/Closure.lean

Modified Mathlib/FieldTheory/Separable.lean

added theorem Subalgebra.isSeparable_iff

added theorem isSeparable_map_iff

Modified Mathlib/FieldTheory/SeparableClosure.lean

added theorem IntermediateField.FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure

added theorem isClosed_restrictScalars_separableClosure

added theorem le_restrictScalars_separableClosure

added theorem separableClosure_le_separableClosure_iff

Modified Mathlib/FieldTheory/SeparableDegree.lean

deleted theorem Field.isSeparable_algebraMap

Modified Mathlib/Logic/Equiv/Basic.lean

added theorem Equiv.image_swap_of_mem_of_notMem

Modified Mathlib/RingTheory/AlgebraicIndependent/Defs.lean

added theorem AlgebraicIndepOn.mono

Modified Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean

added theorem IsTranscendenceBasis.of_isAlgebraic_adjoin_image_compl

added theorem IsTranscendenceBasis.of_isAlgebraic_adjoin_insert_diff