Theorem Ideal.finite_setOf_absNorm_eq

Modification history

2024-10-24 10:44

Mathlib/RingTheory/Ideal/Norm.lean

feat(RingTheory/Ideal/Norm): Generalize `Ideal.finite_setOf_absNorm_eq` and add `Ideal.finite_setOf_absNorm_le` (#18132) …

Modified Ideal.finite_setOf_absNorm_eq View on Github →

2023-06-22 06:58

Mathlib/RingTheory/Ideal/Norm.lean

feat: port RingTheory.Ideal.Norm (#5311)

Added Ideal.finite_setOf_absNorm_eq View on Github →