Theorems · Theorem · linear algebra

Module.Basis.sumQuot_inr

∀ {R : Type u_2} {V : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Submodule R V}
  {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (j : n),
  Submodule.Quotient.mk ((bW.sumQuot bQ) (Sum.inr j)) = bQ j

Defined in

Mathlib.LinearAlgebra.Dimension.Constructions

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule