Theorems · Theorem · linear algebra

Submodule.Quotient.equiv_apply

∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_5} [inst_1 : Ring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M : Type u_6} {N : Type u_7}
  [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N] [inst_7 : Module R₂ N] (P : Submodule R M)
  (Q : Submodule R₂ N) (f : M ≃ₛₗ[σ₁₂] N) (hf : Submodule.map (↑f) P = Q) (a : M ⧸ P),
  (Submodule.Quotient.equiv P Q f hf) a = (P.mapQ Q ↑f ⋯) a

Defined in

Mathlib.LinearAlgebra.Quotient.Basic

Cited by

0 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRingRingHomInvPairRingHomInvPairAddCommGroupModuleAddCommGroupModule