J — Mathlib · SciLib

English

The action J on τ corresponds to neg conj on its complex coordinate.

Русский

Действие J на τ соответствует отрицательному комплексному сопряжению координаты τ.

LaTeX

$$$\forall \tau,\; (J \cdot \tau) = -\overline{\tau}$$$

Lean4

/-- The matrix `[-1, 0; 0, 1]`, which defines an anti-holomorphic involution of `ℍ` via
`τ ↦ -conj τ`. -/
def J : GL (Fin 2) ℝ :=
  .mkOfDetNeZero !![-1, 0; 0, 1] (by simp)

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