Theorems · Theorem · commutative algebra

LinearEquiv.conj_apply

∀ {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [inst : CommSemiring R₁']
  [inst_1 : CommSemiring R₂'] [inst_2 : AddCommMonoid M₁'] [inst_3 : AddCommMonoid M₂'] [inst_4 : Module R₁' M₁']
  [inst_5 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁']
  [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁'),
  e.conj f = (↑e ∘ₛₗ f) ∘ₛₗ ↑e.symm

Defined in

Mathlib.Algebra.Module.Equiv.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAddCommMonoidAddCommMonoidModuleModuleRingHomInvPairRingHomInvPair