Theorems · Theorem · linear algebra

LinearMap.iSup_range_single_eq_iInf_ker_proj

∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] {I J : Set ι},
  IsCompl I J → I.Finite → ⨆ i ∈ I, (LinearMap.single R φ i).range = ⨅ i ∈ J, (LinearMap.proj i).ker

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEq