Theorem FractionalIdeal.zero_of_num_eq_bot

Modification history

2026-01-13 19:40

Mathlib/RingTheory/FractionalIdeal/Basic.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Modified FractionalIdeal.zero_of_num_eq_bot View on Github →

2024-01-17 13:26

Mathlib/RingTheory/FractionalIdeal/Basic.lean

feat: Generalize absNorm to fractional ideals (#9613) …

Added FractionalIdeal.zero_of_num_eq_bot View on Github →