Commit 2024-12-06 08:34 6c1905d5

View on Github →

chore(RingTheory/JacobsonIdeal): split out Polynomial (#19734) Also create a folder RingTheory/Jacobson containing three files Ideal (originally JacobsonIdeal), Ring (original Jacobson), and Polynomial (new). 22 files have transitive imports reduced by 100 or more.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/CharP/LocalRing.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean

Modified Mathlib/LinearAlgebra/Matrix/Ideal.lean

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

Modified Mathlib/RingTheory/Ideal/Over.lean

Renamed Mathlib/RingTheory/JacobsonIdeal.lean to Mathlib/RingTheory/Jacobson/Ideal.lean

deleted theorem Ideal.jacobson_bot_polynomial_le_sInf_map_maximal

deleted theorem Ideal.jacobson_bot_polynomial_of_jacobson_bot

Created Mathlib/RingTheory/Jacobson/Polynomial.lean

added theorem Ideal.jacobson_bot_polynomial_le_sInf_map_maximal

added theorem Ideal.jacobson_bot_polynomial_of_jacobson_bot

Renamed Mathlib/RingTheory/Jacobson.lean to Mathlib/RingTheory/Jacobson/Ring.lean

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

Modified Mathlib/RingTheory/LocalRing/Subring.lean

Modified Mathlib/RingTheory/Nakayama.lean

Modified Mathlib/RingTheory/Nullstellensatz.lean

Modified Mathlib/RingTheory/Valuation/LocalSubring.lean