Theorem Polynomial.Irreducible.hasSeparableContraction

Modification history

2023-12-26 06:12
Mathlib/RingTheory/Polynomial/SeparableDegree.lean
chore(RingTheory/Polynomial/SeparableDegree): add `HasSeparableContraction.isSeparableContraction` and ... (#9272) …
Deleted Polynomial.Irreducible.hasSeparableContractionView on Github →
2023-11-28 15:55
Mathlib/FieldTheory/SeparableDegree.lean
feat(FieldTheory/SeparableDegree): basic definition of separable degree of field extension (#8117) …
Modified Polynomial.Irreducible.hasSeparableContractionView on Github →
2023-05-24 08:50
Mathlib/FieldTheory/SeparableDegree.lean
feat: port FieldTheory.SeparableDegree (#4287)
Added Polynomial.Irreducible.hasSeparableContractionView on Github →