Theorem Ideal.mem_iInf_smul_pow_eq_bot_iff

Modification history

2023-08-16 16:40

Mathlib/RingTheory/Filtration.lean

chore: restate `isNoetherian_of_fg_of_noetherian'` using `Module.Finite` (and rename). (#6609)

Modified Ideal.mem_iInf_smul_pow_eq_bot_iff View on Github →

2023-06-01 12:52

Mathlib/RingTheory/Filtration.lean

feat: port RingTheory.Filtration (#4488)

Added Ideal.mem_iInf_smul_pow_eq_bot_iff View on Github →