Theorems · Theorem · linear algebra

DFinsupp.ker_mapRangeLinearMap

∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] [inst_2 : (i : ι) → AddCommMonoid (β₂ i)]
  [inst_3 : (i : ι) → Module R (β₁ i)] [inst_4 : (i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i),
  (DFinsupp.mapRange.linearMap f).ker =
    Submodule.comap (DFinsupp.coeFnLinearMap R) (Submodule.pi Set.univ fun i => (f i).ker)

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModule