Commit 2025-01-10 18:59 712c9d48

View on Github →

feat: sets of doubling strictly less than 3/2 (#20572) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Combinatorics/Additive/VerySmallDoubling.lean

added theorem Finset.card_inv_mul_of_doubling_lt_three_halves

added theorem Finset.doubling_lt_three_halves

added def Finset.invMulSubgroup

added theorem Finset.invMulSubgroup_eq_inv_mul

added theorem Finset.invMulSubgroup_eq_mul_inv

added theorem Finset.mul_inv_eq_inv_mul_of_doubling_lt_two

added theorem Finset.smul_inv_mul_eq_inv_mul_opSMul

added theorem Finset.smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves

Modified docs/references.bib