Theorems · Theorem · linear algebra

LinearMap.ker_smul

∀ {K : Type u_4} {V : Type u_9} {V₂ : Type u_10} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (a : K), a ≠ 0 → (a • f).ker = f.ker

Defined in

Mathlib.Algebra.Module.Submodule.Ker

Cited by

4 results in Mathlib

Foundations

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

Assumes

SemifieldAddCommMonoidModuleAddCommMonoidModule