_aux_Mathlib_Analysis_Complex_UpperHalfPlane_MoebiusAction___macroRules_UpperHalfPlane_term↑ₘ__1

English

For any g ∈ GL(2,ℝ) and z ∈ ℍ, denom g z ≠ 0.

Русский

Для любых g ∈ GL(2,ℝ) и z ∈ ℍ, denom g z ≠ 0.

LaTeX

$$$$ \\operatorname{denom}(g,z) \\neq 0. $$$$

Lean4

@[scoped macro UpperHalfPlane.«term↑ₘ_»]
public meta def «_aux_Mathlib_Analysis_Complex_UpperHalfPlane_MoebiusAction___macroRules_UpperHalfPlane_term↑ₘ__1» :
    Macro✝ := fun
  | `(↑ₘ$A) => ``(((($A : GL(2, ℝ)⁺) : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) _))
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

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