Theorems · Theorem · linear algebra

iSupIndep.linearEquiv_apply

∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Ring R] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ i, p i = ⊤) (x : Π₀ (i : ι), ↥(p i)),
  (ind.linearEquiv iSup_top) x = (DFinsupp.sumAddHom fun i => (p i).subtype.toAddMonoidHom) x

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqRingAddCommGroupModule