Commit 2023-09-10 03:26 a57bfd63

View on Github →

feat: roots in an algebra (#6740)

Estimated changes

Modified Mathlib/Data/Polynomial/FieldDivision.lean

Modified Mathlib/Data/Polynomial/RingDivision.lean

added theorem Polynomial.aroots_C

added theorem Polynomial.aroots_C_mul

added theorem Polynomial.aroots_C_mul_X_pow

added theorem Polynomial.aroots_X

added theorem Polynomial.aroots_X_pow

added theorem Polynomial.aroots_X_sub_C

added theorem Polynomial.aroots_def

added theorem Polynomial.aroots_monomial

added theorem Polynomial.aroots_mul

added theorem Polynomial.aroots_one

added theorem Polynomial.aroots_pow

added theorem Polynomial.aroots_smul_nonzero

added theorem Polynomial.aroots_zero

added theorem Polynomial.mem_aroots'

added theorem Polynomial.mem_aroots

Modified Mathlib/Data/Polynomial/Splits.lean

Modified Mathlib/FieldTheory/Adjoin.lean

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

Modified Mathlib/FieldTheory/Galois.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Classification.lean

Modified Mathlib/FieldTheory/Minpoly/Field.lean

Modified Mathlib/FieldTheory/Normal.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/FieldTheory/SplittingField/Construction.lean

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/Discriminant.lean

Modified Mathlib/RingTheory/IntegralClosure.lean

Modified Mathlib/RingTheory/Norm.lean

Modified Mathlib/RingTheory/Polynomial/GaussLemma.lean

Modified Mathlib/RingTheory/PowerBasis.lean

Modified Mathlib/RingTheory/Trace.lean