mem_subgroup_iff

Mathlib.Algebra.Order.Archimedean.Class

URI: https://scilib.ai/kg/mathlib#MulArchimedeanClass.mem_subgroup_iff

English

For hs ≠ ⊤, a ∈ subgroup s iff mk a ∈ s.

Русский

Для hs ≠ ⊤ верно: a ∈ subgroup s ⇔ mk a ∈ s.

LaTeX

$$$(hs \\neq \\top) \\Rightarrow (a \\in subgroup s \\iff mk(a) \\in s)$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_subgroup_iff (hs : s ≠ ⊤) : a ∈ subgroup s ↔ mk a ∈ s := by simp [subgroup, subsemigroup, hs]

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

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

Разделы

Аффилиация

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