Commit 2025-04-10 20:47 89ff66b3
View on Github →feat: lemma eval_of_algHom (#23065)
Let k be an integral domain and G an arbitrary finite set.
Then any algebra morphism φ : (G → k) →ₐ[k] k is an evaluation map.
feat: lemma eval_of_algHom (#23065)
Let k be an integral domain and G an arbitrary finite set.
Then any algebra morphism φ : (G → k) →ₐ[k] k is an evaluation map.