Theorems · Theorem · linear algebra

Submodule.comap_smul

∀ {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [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₂) (p : Submodule K V₂) (a : K),
  a ≠ 0 → Submodule.comap (a • f) p = Submodule.comap f p

Defined in

Mathlib.Algebra.Module.Submodule.Map

Cited by

4 results in Mathlib

Foundations

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

Assumes

SemifieldAddCommMonoidModuleAddCommMonoidModule