Theorem Real.norm_exp_sub_one_sub_id_le

Modification history

2025-11-26 02:38
Mathlib/Analysis/Complex/Exponential.lean
feat(CStarAlgebra): the log is operator monotone (#30894) …
Added Real.norm_exp_sub_one_sub_id_leView on Github →