submonoid — Mathlib

English

The submonoid of α consisting of fixed points of M is defined by carrier = fixedPoints M α, with the monoid structure induced from α.

Русский

Подмоноид α, состоящий из фиксированных точек M, задаётся носителем carrier = fixedPoints M α и моноидной структурой, полученной от α.

LaTeX

$$$$ \\text{submonoid}(M, \\alpha) = \\{ a \\in \\alpha \\mid \\forall m \\in M, m \\cdot a = a \\}. $$$$

Lean4

/-- The submonoid of elements fixed under the whole action. -/
def submonoid : Submonoid α where
  carrier := MulAction.fixedPoints M α
  one_mem' := smul_one
  mul_mem' ha hb _ := by rw [smul_mul', ha, hb]

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