Commit 2025-09-02 15:20 206c7bb9

View on Github →

feat(Algebra): principal ideal finite product rings (#27900) Show that ideals in a finite product semiring correspond to tuples of ideals in individual rings. Consequently, a finite product semiring is a PIR if each semiring is. follow-up of #27236

Estimated changes

Modified Mathlib/LinearAlgebra/Span/Defs.lean

added theorem Submodule.IsPrincipal.span_singleton_generator

Modified Mathlib/RingTheory/Ideal/Basic.lean

modified theorem Ideal.mem_pi

modified def Ideal.pi

added theorem Ideal.pi_le_pi_iff

added theorem Ideal.pi_span

added theorem Ideal.single_mem_pi

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.map_evalRingHom_pi

added def Ideal.piOrderIso

Modified Mathlib/RingTheory/Ideal/Prod.lean

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

deleted theorem Submodule.IsPrincipal.span_singleton_generator

added theorem isPrincipalIdealRing_pi_iff