topologicalGroup — Mathlib

English

The special linear group over a topological ring is a topological group.

Русский

Особая линейная группа над топологической кольцом является топологической группой.

LaTeX

$$IsTopologicalGroup(SL(n,R))$$

Lean4

/-- The special linear group over a topological ring is a topological group. -/
instance topologicalGroup : IsTopologicalGroup (SL n R)
    where
  continuous_inv := by simpa [continuous_induced_rng] using continuous_induced_dom.matrix_adjugate
  continuous_mul := by
    simpa only [continuous_induced_rng] using
      (continuous_induced_dom.comp continuous_fst).mul (continuous_induced_dom.comp continuous_snd)

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