Commit 2024-09-25 21:17 88787b21

View on Github →

feat(FieldTheory/Minpoly): remove IsIntegral condition for lemmas (#17080) Remove IsIntegral condition for minpoly.add_algebraMap and minpoly.sub_algebraMap.

Estimated changes

Modified Mathlib/FieldTheory/Minpoly/Field.lean

modified theorem minpoly.add_algebraMap

modified theorem minpoly.sub_algebraMap

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean