Theorem Height.mulHeight_comp_equiv

Modification history

2026-03-04 14:59
Mathlib/NumberTheory/Height/Basic.lean
feat(NumberTheory/Height/Basic): add {mul|log}Height_comp_le, {mul|log}Height_fun_mul_eq (#35408) …
Modified Height.mulHeight_comp_equivView on Github →
2026-01-19 09:42
Mathlib/NumberTheory/Height/Basic.lean
feat(NumberTheory/Height): heights of tuples and finsupps (#33893) …
Added Height.mulHeight_comp_equivView on Github →