cast_addConst_mul_card

Mathlib.Combinatorics.Additive.DoublingConst

URI: https://scilib.ai/kg/mathlib#Finset.cast_addConst_mul_card

English

For finite A,B in G', the product of σ[A,B] with |A| equals the size of A+B: σ[A,B] · |A| = |A+B|.

Русский

Для конечных A,B в группе G' произведение σ[A,B] на |A| равно размеру A+B: σ[A,B]·|A| = |A+B|.

LaTeX

$$$|A+B| = \\sigma[A,B] \\cdot |A|$$$

Lean4

theorem cast_addConst_mul_card (A B : Finset G') : (σ[A, B] * #A : 𝕜) = #(A + B) := by norm_cast;
  exact addConst_mul_card _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru