Theorems · Theorem · ring theory

LinearMap.map_sub

∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S}
  (f : M →ₛₗ[σ] M₂) (x y : M), f (x - y) = f x - f y

Defined in

Mathlib.Algebra.Module.LinearMap.Defs

Cited by

15 results in Mathlib

Foundations

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

Assumes

SemiringSemiringAddCommGroupAddCommGroup