Theorems · Theorem · commutative algebra

LinearEquiv.domMulActCongrRight_symm_apply

∀ {S : Type u_4} {R₁ : Type u_9} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₁' : Type u_15}
  {M₂' : Type u_16} [inst : Semiring R₁] [inst_1 : Semiring R₁'] [inst_2 : Semiring R₂'] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₁'] [inst_5 : AddCommMonoid M₂'] [inst_6 : Module R₁ M₁] [inst_7 : Module R₁' M₁']
  [inst_8 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₁₂' : R₁ →+* R₂'}
  [inst_9 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_10 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_11 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_12 : Semiring S] [inst_13 : Module S M₁]
  [inst_14 : SMulCommClass R₁ S M₁] [inst_15 : RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'] (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂')
  (a : M₁ →ₛₗ[σ₁₂'] M₂'), e₂.domMulActCongrRight.symm a = ((LinearEquiv.refl R₁ M₁).arrowCongrAddEquiv e₂).invFun a

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringSemiringSemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleRingHomInvPairRingHomInvPairRingHomCompTripleSemiringModuleSMulCommClassRingHomCompTriple