symm

Mathlib.RingTheory.Morita.Basic

URI: https://scilib.ai/kg/mathlib#IsMoritaEquivalent.symm

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem symm {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B] (h : IsMoritaEquivalent R A B) :
    IsMoritaEquivalent R B A where cond := h.cond.map <| .symm R

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru