Theorems · Theorem · linear algebra

Submodule.quotientPi_apply

∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (p : (i : ι) → Submodule R (Ms i))
  (a : ((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p) (i : ι),
  (Submodule.quotientPi p) a i = (Submodule.quotientPiLift p (fun i => (p i).mkQ) ⋯) a i

Defined in

Mathlib.LinearAlgebra.Quotient.Pi

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleFintypeDecidableEq