Theorems · Theorem · number theory

Finset.cast_mulConst

∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑(A.mulConst B) = ↑(A * B).card / ↑A.card

Defined in

Mathlib.Combinatorics.Additive.DoublingConst

Cited by

0 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupDecidableEqSemifieldCharZero