Theorems · Inductive type · ring theory

IsLinearMap

(R : Type u) →
  {M : Type v} →
    {M₂ : Type w} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : AddCommMonoid M₂] → [Module R M] → [Module R M₂] → (M → M₂) → Prop

A map f between modules over a semiring is linear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = c • f x. The predicate IsLinearMap R f asserts this property. A bundled version is available with LinearMap, and should be favored over IsLinearMap most of the time.

Defined in

Mathlib.Algebra.Module.LinearMap.Defs

Cited by

41 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModule