Theorem Ideal.disjoint_powers_iff_not_mem

Modification history

2024-05-18 18:12

Mathlib/RingTheory/Ideal/Operations.lean

chore(AlgebraicGeometry/ProjectiveSpectrum/Scheme): Tidy & golf (#12981)

Modified Ideal.disjoint_powers_iff_not_mem View on Github →

2023-07-04 05:50

Mathlib/RingTheory/Jacobson.lean

feat: port RingTheory.Jacobson (#4338)

Added Ideal.disjoint_powers_iff_not_mem View on Github →