Theorem IntermediateField.splits_iff_mem

Modification history

2025-11-20 19:42
Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
feat(Algebra/Polynomial/Splits): remove the `RingHom` argument of `Splits` (#31631)
Modified IntermediateField.splits_iff_memView on Github →
2024-08-23 14:42
Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
feat(FieldTheory/Normal): Intersection of normal extensions is normal (#15290) …
Added IntermediateField.splits_iff_memView on Github →