Theorems · Definition · linear algebra

Submodule.subtype

{R : Type u} →
  {M : Type v} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → {module_M : Module R M} → (p : Submodule R M) → ↥p →ₗ[R] M

Embedding of a submodule p to the ambient space M.

Defined in

Mathlib.Algebra.Module.Submodule.LinearMap

Cited by

480 results in Mathlib

Foundations

Depth 25 from the axioms, rests on 245 definitions · uses propext, Quot.sound

Assumes

SemiringAddCommMonoid