Theorems · Definition · ring theory

LinearMap.toAddMonoidHom

{R : Type u_1} →
  {S : Type u_5} →
    {M₁ : Type u_9} →
      {M₂ : Type u_10} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M₁] →
              [inst_3 : AddCommMonoid M₂] →
                {modM₁ : Module R M₁} → {modM₂ : Module S M₂} → {σ : R →+* S} → (M₁ →ₛₗ[σ] M₂) → M₁ →+ M₂

Convert a linear map to an additive monoid hom.

Defined in

Mathlib.Algebra.Module.LinearMap.Defs

Cited by

101 results in Mathlib

Foundations

Depth 23 from the axioms, rests on 188 definitions · uses propext

Assumes

SemiringSemiringAddCommMonoidAddCommMonoid