Theorems · Theorem · field theory

finrank_algHom

∀ (K : Type u) (V : Type v) [inst : Field K] [inst_1 : Field V] [inst_2 : Algebra K V] [inst_3 : FiniteDimensional K V],
  Fintype.card (V →ₐ[K] V) ≤ Module.finrank V (V →ₗ[K] V)

Defined in

Mathlib.FieldTheory.Fixed

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFiniteDimensional