Commit 2024-08-21 07:40 ed125a42

View on Github →

chore: split FieldTheory/IntermediateField (#15692)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/CharP/IntermediateField.lean

Modified Mathlib/FieldTheory/Adjoin.lean

Created Mathlib/FieldTheory/IntermediateField/Algebraic.lean

added theorem IntermediateField.eq_of_le_of_finrank_eq'

added theorem IntermediateField.eq_of_le_of_finrank_eq

added theorem IntermediateField.eq_of_le_of_finrank_le'

added theorem IntermediateField.eq_of_le_of_finrank_le

added theorem IntermediateField.finrank_eq_finrank_subalgebra

added theorem IntermediateField.isAlgebraic_iff

added theorem IntermediateField.isIntegral_iff

added theorem IntermediateField.minpoly_eq

added theorem IntermediateField.rank_eq_rank_subalgebra

added theorem IntermediateField.toSubalgebra_eq_iff

added theorem mem_subalgebraEquivIntermediateField

added theorem mem_subalgebraEquivIntermediateField_symm

added def subalgebraEquivIntermediateField

Renamed Mathlib/FieldTheory/IntermediateField.lean to Mathlib/FieldTheory/IntermediateField/Basic.lean

deleted theorem IntermediateField.eq_of_le_of_finrank_eq'

deleted theorem IntermediateField.eq_of_le_of_finrank_eq

deleted theorem IntermediateField.eq_of_le_of_finrank_le'

deleted theorem IntermediateField.eq_of_le_of_finrank_le

deleted theorem IntermediateField.finrank_eq_finrank_subalgebra

deleted theorem IntermediateField.isAlgebraic_iff

deleted theorem IntermediateField.isIntegral_iff

deleted theorem IntermediateField.minpoly_eq

deleted theorem IntermediateField.rank_eq_rank_subalgebra

deleted theorem IntermediateField.toSubalgebra_eq_iff

deleted theorem mem_subalgebraEquivIntermediateField

deleted theorem mem_subalgebraEquivIntermediateField_symm

deleted def subalgebraEquivIntermediateField

Modified Mathlib/FieldTheory/NormalClosure.lean

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

Modified Mathlib/LinearAlgebra/JordanChevalley.lean

Modified Mathlib/RingTheory/LittleWedderburn.lean

Modified Mathlib/Topology/Instances/Complex.lean