divConst — Mathlib

English

The difference 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

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

Lean4

/-- The difference 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 difference 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 divConst (A B : Finset G) : ℚ≥0 :=
  #(A / B) / #A

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