mem_subgroup — Mathlib

English

For M a monoid, α a group, a ∈ α fixed by all M iff a ∈ fixedPoints.submonoid M α.

Русский

Для моноида M, группы α, a фиксируется всеми элементами M тогда и только тогда, когда a ∈ fixedPoints.submonoid M α.

LaTeX

$$$$ a \\in \\mathrm{FixedPoints}.\\submonoid M \\alpha \\iff \\forall m : M, m \\cdot a = a. $$$$

Lean4

@[simp]
theorem mem_subgroup (a : α) : a ∈ α^*M ↔ ∀ m : M, m • a = a :=
  Iff.rfl

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