Theorem NumberField.InfiniteAdeleRing.norm_eq_zero_of_not_isUnit

Modification history

2026-07-29 08:07
Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean
feat: notation for adele rings (#40535) …
Modified NumberField.InfiniteAdeleRing.norm_eq_zero_of_not_isUnitView on Github →
2026-03-14 13:07
Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean
feat(NumberTheory/NumberField/InfiniteAdeleRing): norm and product formula for the infinite adele ring (#36204)
Added NumberField.InfiniteAdeleRing.norm_eq_zero_of_not_isUnitView on Github →