Commit 2024-07-27 18:20 cfbc1bd2

View on Github →

chore(Polynomial/UnitTrinomial): Don't import the fundamental theorem of algebra (#15207) Split the one lemma that requires it to a new file Analysis.Complex.Polynomial.UnitTrinomial. Also move Analysis.Complex.Polynomial to Analysis.Complex.Polynomial.Basic.

Estimated changes

Modified Archive/Wiedijk100Theorems/AbelRuffini.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/UnitTrinomial.lean

deleted theorem Polynomial.IsUnitTrinomial.irreducible_of_coprime'

Renamed Mathlib/Analysis/Complex/Polynomial.lean to Mathlib/Analysis/Complex/Polynomial/Basic.lean

Created Mathlib/Analysis/Complex/Polynomial/UnitTrinomial.lean

added theorem Polynomial.IsUnitTrinomial.irreducible_of_coprime'

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Modified Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

Modified Mathlib/RingTheory/Polynomial/Selmer.lean