σ — Mathlib · SciLib

English

For any g,h ∈ GL(2,ℝ) and z ∈ ℂ, σ g (denom h z) = denom h (σ g z).

Русский

Для любых g,h ∈ GL(2,ℝ) и z ∈ ℂ, σ g(denom h z) = denom h(σ g z).

LaTeX

$$$$ \\sigma(g)(\\operatorname{denom}(h,z)) = \\operatorname{denom}(h, \\sigma(g)(z)). $$$$

Lean4

/-- Automorphism of `ℂ`: the identity if `0 < det g` and conjugation otherwise. -/
noncomputable def σ (g : GL (Fin 2) ℝ) : ℂ →+* ℂ :=
  if 0 < g.det.val then RingHom.id ℂ else starRingEnd ℂ

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