Theorem Ideal.mem_pi

Modification history

2025-09-02 15:20
Mathlib/RingTheory/Ideal/Basic.lean
feat(Algebra): principal ideal finite product rings (#27900) …
Modified Ideal.mem_piView on Github →
2025-01-07 11:43
Mathlib/RingTheory/Ideal/Basic.lean
chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535) …
Modified Ideal.mem_piView on Github →
2023-02-21 09:05
Mathlib/RingTheory/Ideal/Basic.lean
feat: port RingTheory.Ideal.Basic (#2283) …
Added Ideal.mem_piView on Github →