Theorems · Theorem · commutative algebra

LinearEquiv.arrowCongr.congr_simp

∀ {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_12} {R₂' : Type u_13} {M₁ : Type u_17} {M₂ : Type u_18}
  {M₁' : Type u_20} {M₂' : Type u_21} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : CommSemiring R₁']
  [inst_3 : CommSemiring R₂'] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid M₁']
  [inst_7 : AddCommMonoid M₂'] [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] [inst_10 : Module R₁' M₁']
  [inst_11 : Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'}
  {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' σ₂₁'_1 : R₂ →+* R₁'} (e_σ₂₁' : σ₂₁' = σ₂₁'_1) {σ₁₂' σ₁₂'_1 : R₁ →+* R₂'}
  (e_σ₁₂' : σ₁₂' = σ₁₂'_1) [inst_12 : RingHomInvPair σ₁₂ σ₂₁] [inst_13 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_15 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂']
  [inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ e₁_1 : M₁ ≃ₛₗ[σ₁₂] M₂),
  e₁ = e₁_1 → ∀ (e₂ e₂_1 : M₁' ≃ₛₗ[σ₁'₂'] M₂'), e₂ = e₂_1 → e₁.arrowCongr e₂ = e₁_1.arrowCongr e₂_1

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringSemiringCommSemiringCommSemiringAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleModuleRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTriple