instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL

Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

URI: https://scilib.ai/kg/mathlib#Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL

English

The image of SL(n,Z) in GL(n,R) is arithmetic.

Русский

Образ SL(n,ℤ) в GL(n,ℝ) является арифметическим.

LaTeX

$$IsArithmetic 𝒮ℒ where 𝒮ℒ is the image of SL(n,Z) in GL(n,R)$$

Lean4

/-- The image of `SL(2, ℤ)` in `GL(2, ℝ)` is arithmetic. -/
instance : IsArithmetic 𝒮ℒ where is_commensurable := .refl 𝒮ℒ

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru