card_mul_mulConst

Mathlib.Combinatorics.Additive.DoublingConst

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

← MathLib Explorer

English

There is a symmetric relation: card(A) · MulConst(A,B) equals |A B|.

Русский

Существует симметричная связь: |A| · MulConst(A,B) = |A B|.

LaTeX

$$$|A| \cdot A.mulConst B = |A B|$$$

Lean4

@[to_additive (attr := simp) card_mul_addConst]
theorem card_mul_mulConst (A B : Finset G) : #A * σₘ[A, B] = #(A * B) := by rw [mul_comm, mulConst_mul_card]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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