is_eqv

Mathlib.Algebra.BrauerGroup.Defs

URI: https://scilib.ai/kg/mathlib#IsBrauerEquivalent.is_eqv

English

The relation IsBrauerEquivalent is an equivalence relation on CSA K.

Русский

Отношение IsBrauerEquivalent образует эквивалентность в отношении центрально простых алгебр над K.

LaTeX

$$IsBrauerEquivalent.is_eqv : Equivalence (IsBrauerEquivalent (K := K))$$

Lean4

theorem is_eqv : Equivalence (IsBrauerEquivalent (K := K))
    where
  refl := refl
  symm := symm
  trans := trans

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

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

Разделы

Аффилиация

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