non-Archimedean non-instances

Mathlib.Topology.Algebra.Nonarchimedean.Bases

URI: https://scilib.ai/kg/mathlib#SubmodulesBasis.Mathlib.LibraryNote.non-Archimedean non-instances

Lean4

/-- The non-Archimedean subgroup basis lemmas cannot be instances because some instances
(such as `MeasureTheory.AEEqFun.instAddMonoid` or `IsTopologicalAddGroup.toContinuousAdd`)
cause the search for `@IsTopologicalAddGroup β ?m1 ?m2`, i.e. a search for a topological group where
the topology/group structure are unknown. -/
def «non-Archimedean non-instances» : LibraryNote✝ :=
  ()

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

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

Разделы

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

Аффилиация

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