Commit 2025-12-17 21:56 7fab5162

View on Github →

chore(Analysis): fix whitespace (#32909) Extracted from https://github.com/leanprover-community/mathlib4/pull/30658. Found by extending the commandStart linter to proof bodies.

Estimated changes

modified theorem cfcₙ_neg
modified theorem cfc_neg
modified theorem HasDerivAt.comp_ringHom
modified theorem Real.enorm_ofReal_of_nonneg
modified theorem SemiNormedGrp.hom_neg
modified theorem WithLp.prod_nnnorm_eq_sup
modified theorem NormedSpace.normalize_neg
modified theorem Real.deriv2_negMulLog
modified theorem Real.negMulLog_eq_neg
modified def Real.mulExpNegMulSq
modified theorem Real.mulExpNegSq_apply
modified theorem NNReal.lt_rpow_inv_iff
modified theorem Real.hasSum_cosh