Theorem Polynomial.algEquivAevalXAddC_symm

Modification history

2024-11-19 08:56
Mathlib/Algebra/Polynomial/AlgebraMap.lean
feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits (#17369) …
Modified Polynomial.algEquivAevalXAddC_symmView on Github →
2024-10-28 06:12
Mathlib/Algebra/Polynomial/AlgebraMap.lean
feat(Algebra/Polynomial/AlgebraMap): add `algEquiv(OfCompEqX|AevalXAddC)_(eq_iff|symm)` (#18257)
Added Polynomial.algEquivAevalXAddC_symmView on Github →