Theorems · Theorem · field theory

cardinalMk_algHom

∀ (K : Type u) (V : Type v) (W : Type w) [inst : Field K] [inst_1 : Ring V] [inst_2 : Algebra K V]
  [FiniteDimensional K V] [inst_4 : Field W] [inst_5 : Algebra K W],
  Cardinal.mk (V →ₐ[K] W) ≤ ↑(Module.finrank W (V →ₗ[K] W))

Defined in

Mathlib.FieldTheory.Fixed

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldRingAlgebraFiniteDimensionalFieldAlgebra