Commit 2024-11-11 15:53 cab580f2

View on Github →

chore: split UFD results out of RingTheory.Polynomial.Basic (#18875)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MvPolynomial/Funext.lean

Modified Mathlib/Algebra/Polynomial/Expand.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean

Modified Mathlib/FieldTheory/PrimitiveElement.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

Modified Mathlib/RingTheory/Artinian.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/DualNumber.lean

Modified Mathlib/RingTheory/EssentialFiniteness.lean

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

Modified Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

Modified Mathlib/RingTheory/Localization/InvSubmonoid.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

deleted theorem Polynomial.exists_irreducible_of_degree_pos

deleted theorem Polynomial.exists_irreducible_of_natDegree_ne_zero

deleted theorem Polynomial.exists_irreducible_of_natDegree_pos

deleted theorem Polynomial.exists_monic_irreducible_factor

Modified Mathlib/RingTheory/Polynomial/GaussLemma.lean

Created Mathlib/RingTheory/Polynomial/UniqueFactorization.lean

added theorem Polynomial.exists_irreducible_of_degree_pos

added theorem Polynomial.exists_irreducible_of_natDegree_ne_zero

added theorem Polynomial.exists_irreducible_of_natDegree_pos

added theorem Polynomial.exists_monic_irreducible_factor

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean