Theorem Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg

Modification history

2026-03-04 14:59
Mathlib/Analysis/Normed/Ring/Basic.lean
feat(NumberTheory/Height/Basic): add {mul|log}Height_comp_le, {mul|log}Height_fun_mul_eq (#35408) …
Added Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonnegView on Github →