Theorems · Theorem · linear algebra

Submodule.factor_comp

∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p p' p'' : Submodule R M} (H1 : p ≤ p') (H2 : p' ≤ p''),
  Submodule.factor H2 ∘ₗ Submodule.factor H1 = Submodule.factor ⋯

Defined in

Mathlib.LinearAlgebra.Quotient.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule