Theorems · Theorem · ring theory

NonUnitalRingHom.ext

∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  ⦃f g : α →ₙ+* β⦄, (∀ (x : α), f x = g x) → f = g

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

21 results in Mathlib

Foundations

Depth 11 from the axioms · uses Quot.sound

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring