Def Polynomial.SplittingFieldAuxAux

Modification history

2024-01-08 09:51
Mathlib/FieldTheory/SplittingField/Construction.lean
chore(*): use α → β instead of ∀ _ : α, β (#9529)
Modified Polynomial.SplittingFieldAuxAuxView on Github →
2023-06-15 07:21
Mathlib/FieldTheory/SplittingField/Construction.lean
feat: port FieldTheory.SplittingField.Construction (#4891)
Added Polynomial.SplittingFieldAuxAuxView on Github →