Mathlib v3 is deprecated. Go to Mathlib v4

Def ideal.rel_norm

Modification history

2023-02-03 19:48

src/ring_theory/ideal/norm.lean

feat(ring_theory/ideal/norm): relative ideal norm (#18303) …

Added ideal.rel_norm View on Github →