Theorem Algebra.intNorm_ne_zero

Modification history

2025-12-07 22:48

Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

chore(RingTheory): generalize `Algebra.intNorm` (#32542) …

Modified Algebra.intNorm_ne_zero View on Github →

2024-01-09 09:24

Mathlib/RingTheory/IntegralRestrict.lean

feat: Define `intNorm` and `intTrace`. (#9265)

Added Algebra.intNorm_ne_zero View on Github →