Commit 2025-08-24 11:37 40d9b7a4

View on Github →

chore(Algebra/Order/Nonneg/Module): don't import Finset (#28851) This way we can import it in Data.NNReal.Defs in #28817.

Estimated changes

modified theorem Nonneg.coe_smul
modified theorem Nonneg.mk_smul