Theorems · Definition · ring theory

LinearMap.finiteRange

(K : Type u_1) →
  (V : Type u_2) →
    (V₂ : Type u_4) →
      [inst : CommRing K] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module K V] → [inst_3 : AddCommGroup V₂] → [inst_4 : Module K V₂] → Submodule K (V →ₗ[K] V₂)

LinearMap.finiteRange is the submodule of V →ₗ[K] W consisting of linear maps satisfying LinearMap.HasNoetherianRange. We allow ourself this slightly abusive name because the set of linear maps satisfying LinearMap.HasFiniteRange is only a submodule over a noetherian ring, in which case the two notions agree.

Defined in

Mathlib.Algebra.Module.LinearMap.FiniteRange

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModule