continuous_det

Mathlib.Topology.Instances.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.GeneralLinearGroup.continuous_det

← MathLib Explorer

English

The determinant map det: GL(n,R) → R× is continuous.

Русский

Детерминантная карта det: GL(n,R) → R× непрерывна.

LaTeX

$$Continuous(det : GL(n,R) → R×)$$

Lean4

/-- The determinant is continuous as a map from the general linear group to the units. -/
@[continuity, fun_prop]
protected theorem continuous_det : Continuous (det : GL n R → Rˣ) :=
  by
  simp_rw [Units.continuous_iff, ← map_inv]
  constructor <;> fun_prop

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

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

Разделы

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

Аффилиация

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