Theorems · Theorem · linear algebra

AlgHom.eq_piEvalAlgHom

∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [NoZeroDivisors k] [Nontrivial k] [Finite G]
  (φ : (G → k) →ₐ[k] k), ∃ s, φ = Pi.evalAlgHom k (fun i => k) s

Let k be an integral domain and G an arbitrary finite set. Then any algebra morphism φ : (G → k) →ₐ[k] k is an evaluation map.

Defined in

Mathlib.LinearAlgebra.StdBasis

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringNoZeroDivisorsNontrivialFinite