Commit 2024-10-30 18:46 9889933d

View on Github →

chore({Finset,Multiset}/Lattice): add gcongr attributes (#18451) Added @[gcongr] attributes to Finset.sup_mono_fun, Multiset.sup_mono, and the corresponding theorems with inf.

Estimated changes