Theorems · Theorem · ring theory

LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent

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

Over a domain R, an endomorphism f of a free module V of rank ≠ 1 such that f v and v are collinear, for all v : V, consists of homotheties with central ratio. When R does not satisfy StrongRankCondition, use LinearMap.exists_mem_center_apply_eq_smul_of_basis. When finrank R V = 1, up to a linear equivalence V ≃ₗ[R] R, then any f is right-multiplication by some a : R, but not necessarily left-multiplication by an element of the center of R.

Defined in

Mathlib.LinearAlgebra.Center

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingIsDomainStrongRankConditionAddCommGroupModuleModule.Free