Def Finset.mulConst

Modification history

2024-10-22 13:55

Mathlib/Combinatorics/Additive/DoublingConst.lean

chore(Combinatorics): use newly introduced finset notation (#18055) …

Modified Finset.mulConst View on Github →

2024-08-16 17:37

Mathlib/Combinatorics/Additive/DoublingConst.lean

feat: Doubling and difference constants of two finsets (#15882) …

Added Finset.mulConst View on Github →