Commit 2026-04-04 20:14 f51efbe0

View on Github →

feat: use a constructor for NNReal (#37609) Currently, many elements of NNReal are constructed as pair (x, hx), i.e., as elements of the subtype of nonnegative real numbers. The two types are defeq, but not reducibly, so this creates many defeq abuses. This PR introduces a constructor NNReal.mk and uses it instead of the bare constructor, to avoid these defeq abuses.

Estimated changes

modified theorem Complex.nnnorm_nnratCast
modified theorem Real.nnnorm_nnratCast
modified theorem Real.nnnorm_of_nonneg
modified theorem RCLike.nnnorm_nnratCast
modified theorem NNReal.coe_mk
added theorem NNReal.inv_mk
modified theorem NNReal.mk_natCast
modified theorem NNReal.mk_one
modified theorem NNReal.mk_zero
modified theorem NNReal.smul_def
modified theorem Real.toNNReal_of_nonneg
added theorem Measurable.nnreal_mk