Commit 2024-08-31 13:47 ef885793

View on Github →

feat(ENNReal): Scalar multiplication by NNReal is finite (#16319) From LeanAPAP

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/Module/Defs.lean

Modified Mathlib/Analysis/Normed/Group/Quotient.lean

Modified Mathlib/Data/ENNReal/Operations.lean

added theorem ENNReal.nnreal_smul_lt_top

added theorem ENNReal.nnreal_smul_lt_top_iff

added theorem ENNReal.nnreal_smul_ne_top

added theorem ENNReal.nnreal_smul_ne_top_iff

Modified Mathlib/Data/NNReal/Basic.lean

added theorem NNReal.mk_one

added theorem NNReal.mk_zero

Modified Mathlib/Data/Real/Sqrt.lean

modified theorem Real.sqrt_nonneg