Theorems · Theorem · linear algebra

cardinalMk_algHom_le_rank

∀ (K : Type u_1) (M : Type u_2) (L : Type v) [inst : CommRing K] [inst_1 : Ring M] [inst_2 : Algebra K M]
  [Module.Free K M] [Module.Finite K M] [inst_5 : CommRing L] [IsDomain L] [inst_7 : Algebra K L],
  Cardinal.mk (M →ₐ[K] L) ≤ Cardinal.lift.{v, u_2} (Module.rank K M)

Defined in

Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingRingAlgebraModule.FreeModule.FiniteCommRingIsDomainAlgebra