instDiscreteTopology

Mathlib.Topology.Instances.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.SpecialLinearGroup.instDiscreteTopology

← MathLib Explorer

English

The natural map from SL(n,R) to GL(n,R) is continuous.

Русский

Естественная карта из SL(n,R) в GL(n,R) непрерывна.

LaTeX

$$Continuous(toGL : SL(n,R) → GL(n,R))$$

Lean4

/-- If `R` is a commutative ring with the discrete topology, then `SL(n, R)` has the discrete
topology. -/
instance [DiscreteTopology R] : DiscreteTopology (SL n R) :=
  instDiscreteTopologySubtype

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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