is_invariant_one' — Mathlib

English

The constant function 1 is invariant under the SL(2,ℤ) slash action for any A ∈ SL(2,ℤ) when viewed in GL(2,ℝ).

Русский

Пусть константная функция 1; она инвариантна относительно slash-действия SL(2,ℤ) при восприятии как элемента GL(2,ℝ).

LaTeX

$$$ (1 \lvert[0] A) = 1 $ for all A ∈ SL(2,ℤ)$$

Lean4

/-- Variant of `is_invariant_one` with the left-hand side in simp normal form. -/
@[simp]
theorem is_invariant_one' (A : SL(2, ℤ)) : (1 : ℍ → ℂ) ∣[(0 : ℤ)] (A : GL (Fin 2) ℝ) = 1 := by
  simpa using is_invariant_one A

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