mulConst_inv_left — Mathlib

English

The doubling constant is bounded above by the square of the difference constant: σ_m[A] ≤ δ_m[A]^2.

Русский

Константа удвоения ограничена сверху квадратом константы различий: σ_m[A] ≤ δ_m[A]^2.

LaTeX

$$\\sigma_m[A] \\le \\delta_m[A]^2$$

Lean4

@[to_additive (attr := simp)]
theorem mulConst_inv_left (A B : Finset G) : σₘ[A⁻¹, B] = δₘ[A, B] := by
  rw [mulConst, divConst, card_inv, ← card_inv, mul_inv_rev, inv_inv, inv_mul_eq_div]

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