to_isTopologicalDivisionRing

Mathlib.Analysis.Normed.Field.Lemmas

URI: https://scilib.ai/kg/mathlib#NormedDivisionRing.to_isTopologicalDivisionRing

← MathLib Explorer

English

A normed division ring is a topological division ring.

Русский

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

LaTeX

$$$\text{IsTopologicalDivisionRing}(\alpha)$$$

Lean4

/-- A normed division ring is a topological division ring. -/
instance (priority := 100) to_isTopologicalDivisionRing : IsTopologicalDivisionRing α where

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

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

Разделы

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

Аффилиация

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