Theorem Nonneg.coe_smul

Modification history

2025-08-24 11:37
Mathlib/Algebra/Order/Nonneg/Module.lean
chore(Algebra/Order/Nonneg/Module): don't import `Finset` (#28851) …
Modified Nonneg.coe_smulView on Github →
2023-09-29 03:32
Mathlib/Algebra/Order/Nonneg/Module.lean
feat(Analysis): define pointed cones (#6437) …
Added Nonneg.coe_smulView on Github →