instAlgebra

Mathlib.NumberTheory.NumberField.InfinitePlace.Completion

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.Completion.instAlgebra

English

The completion v.Completion carries a natural structure of a K-algebra.

Русский

Дополнение v.Completion имеет естественную структуру K-алгебры.

LaTeX

$$Algebra K v.Completion$$

Lean4

instance : Algebra K v.Completion :=
  inferInstanceAs <| Algebra (WithAbs v.1) v.1.Completion

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

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

Разделы

Аффилиация

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