Theorem Real.enorm_ofReal_of_nonneg

Modification history

2025-12-17 21:56
Mathlib/Analysis/Normed/Group/Basic.lean
chore(Analysis): fix whitespace (#32909) …
Modified Real.enorm_ofReal_of_nonnegView on Github →
2025-05-15 14:33
Mathlib/Analysis/Normed/Group/Basic.lean
chore(LpSeminorm/Basic): golf a norm lemma using its enorm equivalent (#24814) …
Added Real.enorm_ofReal_of_nonnegView on Github →