Theorem NNReal.coe_nonneg

Modification history

2024-08-06 23:04

Mathlib/Data/NNReal/Basic.lean

feat(Tactic.Bound): Add a `bound` tactic for inequalities by structure (#10562) …

Modified NNReal.coe_nonneg View on Github →

2023-02-20 08:04

Mathlib/Data/Real/NNReal.lean

feat: port Data.Real.NNReal (#2234)

Added NNReal.coe_nonneg View on Github →