refl

Mathlib.RingTheory.Morita.Basic

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

English

For any R-algebra A, A is Morita equivalent to itself via the identity Morita equivalence.

Русский

Для любой R-алгебры A A Морита эквивалентна самой себе через тождественную эквивалентность Мориты.

LaTeX

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

Lean4

theorem refl (A : Type u₁) [Ring A] [Algebra R A] : IsMoritaEquivalent R A A where cond := ⟨.refl R A⟩

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

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

Разделы

Аффилиация

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