Theorem Real.abs_posLog_mul_sub_posLog_le_posLog_add_posLog

Modification history

2026-09-18 15:04
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
feat: invariance of the characteristic function under Moebius transformations (#43847) …
Added Real.abs_posLog_mul_sub_posLog_le_posLog_add_posLogView on Github →