term↑ₘ[_]_ — Mathlib

Lean4
/-- The coercion into an element of  `GL(2, R)` and finally a 2 × 2 matrix over `R`. This is
similar to `↑ₘ`, but without positivity requirements, and allows the user to specify the ring `R`,
which can be useful to help Lean elaborate correctly.

This notation is scoped in namespace `UpperHalfPlane`. -/
@[scoped term_parser 1000]
public meta def «term↑ₘ[_]_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `UpperHalfPlane.«term↑ₘ[_]_» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "↑ₘ[") (ParserDescr.cat✝ `term 0)) (ParserDescr.symbol✝ "]"))
      (ParserDescr.cat✝ `term 1024))
Похожие утверждения