mem_one

Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

English

For any α with a monoid structure, 1 ∈ Finset α is equivalent to the element 1 belonging to the Finset.

Русский

Для любых α с моноидной структурой, 1 ∈ Finset α эквивалентно тому, что элемент 1 принадлежит финсетному множеству.

LaTeX

$$$1 \in (1 : Finset α)$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_one : a ∈ (1 : Finset α) ↔ a = 1 :=
  mem_singleton

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

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

Разделы

Аффилиация

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