mulConst_mul_card — Mathlib

English

The relation between the doubling constant and the cardinality is σ_m[A,B] * |A| = |A B|.

Русский

Связь между удвоительной константой и кардинальностью: σ_m[A,B] · |A| = |A B|.

LaTeX

$$$|A| \cdot \sigma_m[A,B] = |A B|$$$

Lean4

@[to_additive (attr := simp) addConst_mul_card]
theorem mulConst_mul_card (A B : Finset G) : σₘ[A, B] * #A = #(A * B) :=
  by
  obtain rfl | hA := A.eq_empty_or_nonempty
  · simp
  · exact div_mul_cancel₀ _ (by positivity)

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