Theorem NumberField.InfiniteAdeleRing.coe_norm_eq_abs_norm

Modification history

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.coe_norm_eq_abs_normView on Github →