trans — Mathlib

English

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

Русский

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

LaTeX

$$$ \text{IsMoritaEquivalent}(R,A,B) \to \text{IsMoritaEquivalent}(R,B,C) \to \text{IsMoritaEquivalent}(R,A,C)$$$

Lean4

theorem trans {A B C : Type u₁} [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C]
    (h : IsMoritaEquivalent R A B) (h' : IsMoritaEquivalent R B C) : IsMoritaEquivalent R A C where
  cond := Nonempty.map2 (.trans R) h.cond h'.cond

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