Theorems · Theorem · ring theory

MoritaEquivalence.mk.inj

∀ {R : Type u₀} {inst : CommSemiring R} {A : Type u₁} {inst_1 : Ring A} {inst_2 : Algebra R A} {B : Type u₂}
  {inst_3 : Ring B} {inst_4 : Algebra R B} {eqv : ModuleCat A ≌ ModuleCat B}
  {linear : autoParam (CategoryTheory.Functor.Linear R eqv.functor) MoritaEquivalence.linear._autoParam}
  {eqv_1 : ModuleCat A ≌ ModuleCat B}
  {linear_1 : autoParam (CategoryTheory.Functor.Linear R eqv_1.functor) MoritaEquivalence.linear._autoParam},
  { eqv := eqv, linear := linear } = { eqv := eqv_1, linear := linear_1 } → eqv = eqv_1

Defined in

Mathlib.RingTheory.Morita.Basic

Cited by

1 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Quot.sound