mulConst — Mathlib

English

The doubling constant σ_m(A,B) of two finsets A and B in a group is |A B| / |A|.

Русский

Удвоительная константа σ_m(A,B) двух конечных множеств A, B в группе равна |A B| / |A|.

LaTeX

$$$\sigma_m[A,B] = \dfrac{|A B|}{|A|}$$$

Lean4

/-- The doubling constant `σₘ[A, B]` of two finsets `A` and `B` in a group is `|A * B| / |A|`.

The notation `σₘ[A, B]` is available in scope `Combinatorics.Additive`. -/
@[to_additive /-- The doubling constant `σ[A, B]` of two finsets `A` and `B` in a group is `|A + B| / |A|`.

    The notation `σ[A, B]` is available in scope `Combinatorics.Additive`. -/
    ]
def mulConst (A B : Finset G) : ℚ≥0 :=
  #(A * B) / #A

Похожие утверждения