Theorems · Theorem · linear algebra

Matrix.isRepresentation.toEnd_exists_mem_ideal

∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : Module R M] (b : ι → M) [inst_4 : DecidableEq ι] (hb : Submodule.span R (Set.range b) = ⊤)
  (f : Module.End R M) (I : Ideal R),
  LinearMap.range f ≤ I • ⊤ → ∃ M_1, (Matrix.isRepresentation.toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeAddCommGroupCommRingModuleDecidableEq