Theorem Polynomial.HasSeparableContraction.isSeparableContraction

Modification history

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