nonempty

Mathlib.Combinatorics.Additive.ApproximateSubgroup

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

English

If A is a K-approximate subgroup, then A is nonempty.

Русский

Если A является K-приближённой подпгруппой, то A непусто.

LaTeX

$$$A \\neq \\varnothing$$$

Lean4

@[to_additive]
theorem nonempty (hA : IsApproximateSubgroup K A) : A.Nonempty :=
  ⟨1, hA.one_mem⟩

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

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

Разделы

Аффилиация

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