Theorems · Definition · commutative algebra

LinearMap.submoduleImage

{R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {M' : Type u_10} →
            [inst_3 : AddCommMonoid M'] →
              [inst_4 : Module R M'] → {O : Submodule R M} → (↥O →ₗ[R] M') → Submodule R M → Submodule R M'

If O is a submodule of M, and Φ : O →ₗ M' is a linear map, then (ϕ : O →ₗ M').submoduleImage N is ϕ(N) as a submodule of M'

Defined in

Mathlib.Algebra.Module.Submodule.Range

Cited by

7 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule