symm — Mathlib

English

If A is Morita equivalent to B, then B is Morita equivalent to A.

Русский

Если A Морита-эквивалентна B, то B Морита-эквивалентна A.

LaTeX

$$MoritaEquivalence.symm R A B (e : MoritaEquivalence R A B)$$

Lean4

/-- For any `R`-algebras `A` and `B`, if `A` is Morita equivalent to `B`, then `B` is Morita equivalent
to `A`.
-/
def symm {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B] (e : MoritaEquivalence R A B) :
    MoritaEquivalence R B A where
  eqv := e.eqv.symm
  linear := e.eqv.inverseLinear R

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