feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits #62497
Annotations
1 error
|
lint:
Mathlib/Algebra/Polynomial/AlgebraMap.lean#L574
Mathlib/Algebra/Polynomial/AlgebraMap.lean:574 ERR_IND: If the theorem/def statement requires multiple lines, indent it correctly (4 spaces or 2 for `|`)
|
Loading