cast_divConst_mul_card

Mathlib.Combinatorics.Additive.DoublingConst

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

English

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

Русский

Для конечных A,B в G произведение |A| и δ[A,B] равно |A/B|.

LaTeX

$$|A| · δ[A,B] = |A/B|$$

Lean4

@[simp]
theorem cast_divConst_mul_card (A B : Finset G) : (δₘ[A, B] * #A : 𝕜) = #(A / B) := by norm_cast;
  exact divConst_mul_card _ _

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

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

Разделы

Аффилиация

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