Theorem NumberField.sum_nonarchAbsVal_eq

Modification history

2026-03-02 16:30
Mathlib/NumberTheory/Height/NumberField.lean
feat(NumberTheory/Height): formula for logHeight₁ (#35919) …
Added NumberField.sum_nonarchAbsVal_eqView on Github →