Commit 2025-01-07 11:43 01b6f1b3

View on Github →

chore(Ideal/Basic): dependent generalization of Ideal.pi (#20535) Also golf some proofs. TODO: similar to Ideal.idealProdEquiv, we may construct OrderEmbedding from Πᵢ Ideal Rᵢ to Ideal (Πᵢ Rᵢ), which is an OrderIso if the indexing type is finite. This can then be used to show e.g. that a finite product of Noetherian rings is Noetherian without using an inductive argument.

Estimated changes

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Modified Mathlib/RingTheory/Ideal/Basic.lean

modified theorem Ideal.mem_pi

modified def Ideal.pi

Modified Mathlib/RingTheory/Ideal/Quotient/Basic.lean