rclike

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#IsRCLikeNormedField.rclike

Lean4

/-- Given a normed field `𝕜` satisfying `IsRCLikeNormedField 𝕜`, build an associated `RCLike 𝕜`
structure on `𝕜` which is definitionally compatible with the given normed field structure. -/
noncomputable def rclike (𝕜 : Type*) [hk : NormedField 𝕜] [h : IsRCLikeNormedField 𝕜] : RCLike 𝕜 :=
  by
  choose p hp using h.out
  exact p.copy_of_normedField hk hp

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

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

Разделы

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

Аффилиация

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