Theorems · Theorem · ring theory

LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent

∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  [Module.Free R V] {f : V →ₗ[R] V}, (∀ (v : V), ¬LinearIndependent R ![v, f v]) → ∃ a, f = a • 1

Over a commutative domain, an endomorphism f of a free module V such that f v and v are collinear, for all v : V, consists of homotheties.

Defined in

Mathlib.LinearAlgebra.Center

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainAddCommGroupModuleModule.Free