symm — Mathlib

English

Brauer equivalence is symmetric: if A is Brauer equivalent to B, then B is Brauer equivalent to A.

Русский

Эквивалентность Браура симметрична: если A эквивалентна B, то B эквивалентна A.

LaTeX

$$IsBrauerEquivalent(A,B) \Rightarrow IsBrauerEquivalent(B,A)$$

Lean4

@[symm]
theorem symm {A B : CSA K} (h : IsBrauerEquivalent A B) : IsBrauerEquivalent B A :=
  let ⟨n, m, hn, hm, ⟨iso⟩⟩ := h
  ⟨m, n, hm, hn, ⟨iso.symm⟩⟩

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