Theorem Finsupp.logHeight_eq_log_mulHeight

Modification history

2026-01-19 09:42
Mathlib/NumberTheory/Height/Basic.lean
feat(NumberTheory/Height): heights of tuples and finsupps (#33893) …
Added Finsupp.logHeight_eq_log_mulHeightView on Github →