Theorems · Theorem · linear algebra

Submodule.Quotient.equiv.congr_simp

∀ {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 f_1 : M ≃ₛₗ[σ₁₂] N) (e_f : f = f_1) (hf : Submodule.map (↑f) P = Q),
  Submodule.Quotient.equiv P Q f hf = Submodule.Quotient.equiv P Q f_1 ⋯

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