Theorems · Theorem · ring theory

SkewMonoidAlgebra.ringHom_ext

∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k]
  {f g : SkewMonoidAlgebra k G →+* k},
  (∀ (b : k), f (SkewMonoidAlgebra.single 1 b) = g (SkewMonoidAlgebra.single 1 b)) →
    (∀ (a : G), f (SkewMonoidAlgebra.single a 1) = g (SkewMonoidAlgebra.single a 1)) → f = g

If two ring homomorphisms from SkewMonoidAlgebra k G are equal on all single a 1 and single 1 b, then they are equal.

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringMonoidMulSemiringAction