CSA_Setoid — Mathlib

English

Central simple algebras over K form a setoid under Brauer equivalence.

Русский

Центрально простые алгебры над K образуют множество по эквивалентности Браура.

LaTeX

$$Brauer.CSA_Setoid(K) : Setoid (CSA K) with r := IsBrauerEquivalent and iseqv := IsBrauerEquivalent.is_eqv$$

Lean4

/-- `CSA` equipped with Brauer Equivalence is indeed a setoid. -/
def CSA_Setoid : Setoid (CSA K) where
  r := IsBrauerEquivalent
  iseqv := IsBrauerEquivalent.is_eqv

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