Theorems · Theorem · ring theory

LinearMap.zero_apply

∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} (x : M), 0 x = 0

Defined in

Mathlib.Algebra.Module.LinearMap.Defs

Cited by

35 results in Mathlib

Foundations

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

Assumes

SemiringSemiringAddCommMonoidAddCommMonoidModuleModule