coe_apply_complex — Mathlib

English

The entries of the image under the embedding are the corresponding complex numbers equal to the entries of g treated as complex integers: the (i,j)-entry matches g_{i j} in ℂ.

Русский

Элементы изображения под встраиванием coincide с соответствующими комплексными числами: i,j-й элемент равен g_{i j} интерпретированному как комплексное число.

LaTeX

$$$(\mathrm{coe} g)_{i j} = (g_{i j}) \in \mathbb{C}$$$

Lean4

@[simp]
theorem coe_apply_complex {g : SL(2, ℤ)} {i j : Fin 2} :
    (Units.val <| Subtype.val <| coe g) i j = (Subtype.val g i j : ℂ) :=
  rfl

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