Theorems · Theorem · group theory

DistribMulActionHom.ext_ring

∀ {R : Type u_10} [inst : Semiring R] {S : Type u_11} [inst_1 : Semiring S] {N' : Type u_13} [inst_2 : AddMonoid N']
  [inst_3 : DistribMulAction S N'] {σ : R →* S} {f g : R →ₑ+[σ] N'}, f 1 = g 1 → f = g

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

4 results in Mathlib

Foundations

Depth 18 from the axioms · uses Quot.sound

Assumes

SemiringSemiringAddMonoidDistribMulAction