Commit 2024-02-14 01:35 ca018e18

View on Github →

feat: Finset.nsmul_inf' (#9838)

Estimated changes

Modified Mathlib/Data/Finset/Lattice.lean

added theorem Finset.nsmul_inf'

added theorem Finset.nsmul_sup'