Theorems · Theorem · commutative algebra

Module.AEval.isTorsion_of_finiteDimensional

∀ (K : Type u_2) (M : Type u_3) {A : Type u_4} (a : A) [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A]
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module K M] [inst_6 : IsScalarTower K A M]
  [FiniteDimensional K A], Module.IsTorsion (Polynomial K) (Module.AEval K M a)

Defined in

Mathlib.Algebra.Polynomial.Module.FiniteDimensional

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldRingAlgebraAddCommGroupModuleModuleIsScalarTowerFiniteDimensional