Theorem Irreducible.hasSeparableContraction

Modification history

2023-12-26 06:12
Mathlib/RingTheory/Polynomial/SeparableDegree.lean
chore(RingTheory/Polynomial/SeparableDegree): add `HasSeparableContraction.isSeparableContraction` and ... (#9272) …
Added Irreducible.hasSeparableContractionView on Github →