term_^*_ — Mathlib

English

The subgroup of fixed points is compatible with the underlying submonoid of fixed points.

Русский

Подмножество фиксированных точек совместимо с базовым подмоноидом фиксированных точек.

LaTeX

$$$$ (\\mathrm{FixedPoints}.\\text{subgroup } M \\alpha) \\text{.toSubmonoid} = \\mathrm{FixedPoints}.\\submonoid M \\alpha. $$$$

Lean4

/-- The notation for `FixedPoints.subgroup`, chosen to resemble `αᴹ`. -/
@[scoped term_parser 1000]
public meta def «term_^*_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `FixedPoints.«term_^*_» 1022 0
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "^*") (ParserDescr.cat✝ `term 51))

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