instCoeSortCSAType

Mathlib.Algebra.BrauerGroup.Defs

URI: https://scilib.ai/kg/mathlib#instCoeSortCSAType

English

For any field K, each central simple K-algebra A can be regarded as a type via its carrier set A.carrier.

Русский

Для поля K каждый центрально простой K-алгебра A может рассматриваться как тип по егоcarrier.

LaTeX

$$$A \mapsto A_{carrier} : \mathrm{CSA}(K) \to \mathbf{Type}$$$

Lean4

instance : CoeSort (CSA.{u, v} K) (Type v) :=
  ⟨(·.carrier)⟩

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

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

Разделы

Аффилиация

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