card_mul_self_le

Mathlib.Combinatorics.Additive.ApproximateSubgroup

URI: https://scilib.ai/kg/mathlib#IsApproximateSubgroup.card_mul_self_le

← MathLib Explorer

English

For a finite A, #(A*A) ≤ K * #A.

Русский

Для конечного A имеет место #(A*A) ≤ K · #A.

LaTeX

$$$\\ #(A * A) \\le K \\cdot \\#A$$$

Lean4

@[to_additive]
theorem card_mul_self_le [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K (A : Set G)) :
    #(A * A) ≤ K * #A := by simpa [sq] using hA.card_pow_le (n := 2)

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

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

Разделы

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

Аффилиация

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