Commit 2025-02-10 20:18 5ba6c809

View on Github →

feat(RingTheory): Hausdorff-ness of Noetherian rings (#20425)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/AdicCompletion/Noetherian.lean

added theorem IsHausdorff.of_isDomain

added theorem IsHausdorff.of_isLocalRing

added theorem IsHausdorff.of_le_jacobson

added theorem IsHausdorff.of_noZeroSMulDivisors

Modified Mathlib/RingTheory/Filtration.lean

added theorem Ideal.iInf_pow_smul_eq_bot_of_le_jacobson

added theorem Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors