Theorems · Theorem · commutative algebra

LinearEquiv.arrowCongr_comp

∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_12} {R₂' : Type u_13} {R₁'' : Type u_15} {R₂'' : Type u_16}
  {M₁ : Type u_17} {M₂ : Type u_18} {M₁' : Type u_20} {M₂' : Type u_21} {M₁'' : Type u_23} {M₂'' : Type u_24}
  [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : CommSemiring R₁'] [inst_3 : CommSemiring R₂']
  [inst_4 : CommSemiring R₁''] [inst_5 : CommSemiring R₂''] [inst_6 : AddCommMonoid M₁] [inst_7 : AddCommMonoid M₂]
  [inst_8 : AddCommMonoid M₁'] [inst_9 : AddCommMonoid M₂'] [inst_10 : AddCommMonoid M₁'']
  [inst_11 : AddCommMonoid M₂''] [inst_12 : Module R₁ M₁] [inst_13 : Module R₂ M₂] [inst_14 : Module R₁' M₁']
  [inst_15 : Module R₂' M₂'] [inst_16 : Module R₁'' M₁''] [inst_17 : Module R₂'' M₂''] {σ₁₂ : R₁ →+* R₂}
  {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁''₂'' : R₁'' →+* R₂''} {σ₂''₁'' : R₂'' →+* R₁''}
  {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₁'₁'' : R₁' →+* R₁''} {σ₂'₂'' : R₂' →+* R₂''} {σ₁₁'' : R₁ →+* R₁''}
  {σ₂₂'' : R₂ →+* R₂''} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} {σ₂'₁'' : R₂' →+* R₁''} {σ₁'₂'' : R₁' →+* R₂''}
  {σ₂₁'' : R₂ →+* R₁''} {σ₁₂'' : R₁ →+* R₂''} [inst_18 : RingHomInvPair σ₁₂ σ₂₁] [inst_19 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_20 : RingHomInvPair σ₁'₂' σ₂'₁'], ⋯

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringSemiringCommSemiringCommSemiringCommSemiringCommSemiringAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleModuleModuleModuleRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTriple