English
The opposite algebra of a central algebra is central: If IsCentral K D, then IsCentral K Dᵐᵒᵖ.
Русский
Обратная алгебра центральной алгебры также центральна: IsCentral K Dᵐᵒᵖ при IsCentral K D.
LaTeX
$$$\\forall (K D):\\mathrm{Type},\\; IsCentral\\ K D \\Rightarrow IsCentral\\ K D^{\\mathrm{op}}$$$
Lean4
/-- Opposite algebra of a central algebra is central. This instance combined with the coming
`IsSimpleRing` instance for the opposite of central simple algebra will be an
inverse for an element in `BrauerGroup`, find out more about this in
`Mathlib/Algebra/BrauerGroup/Basic.lean`. -/
instance : IsCentral K Dᵐᵒᵖ where
out z
hz :=
have ⟨k, hk⟩ := h.1 (MulOpposite.unop_mem_center_iff.mpr hz)
⟨k, by simpa using congr(op $hk)⟩
