isUnit_iff_singleton

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.isUnit_iff_singleton

English

In a Group, IsUnit f iff there exists a such that f = pure a.

Русский

В группе IsUnit f эквивалентно существованию a such that f = pure a.

LaTeX

$$IsUnit f ↔ ∃ a, f = pure a$$

Lean4

@[simp]
theorem isUnit_iff_singleton : IsUnit f ↔ ∃ a, f = pure a := by simp only [isUnit_iff, Group.isUnit, and_true]

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

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

Разделы

Аффилиация

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