term↑ₘ_ — Mathlib

English

If τ ∈ ℍ and cd ∈ Fin 2 → ℝ with cd ≠ 0, then (cd0) τ + cd1 ≠ 0.

Русский

Если τ ∈ ℍ и cd ∈ Fin 2 → ℝ с cd ≠ 0, то (cd0) τ + cd1 ≠ 0.

LaTeX

$$$$ (cd_0) \\tau + cd_1 \\neq 0, \\quad \\tau \\in \\mathbb{H}. $$$$

Lean4

/-- The coercion first into an element of  `GL(2, ℝ)⁺`, then  `GL(2, ℝ)` and finally a 2 × 2
matrix.

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.symbol✝ "↑ₘ") (ParserDescr.cat✝ `term 1024))

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