Theorems · Theorem · commutative algebra

MonoidWithZeroHom.ext_int

∀ {M : Type u_5} [inst : MonoidWithZero M] {f g : ℤ →*₀ M},
  f (-1) = g (-1) → f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom → f = g

If two MonoidWithZeroHoms agree on -1 and the naturals then they are equal.

Defined in

Mathlib.Data.Int.Cast.Lemmas

Cited by

2 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Quot.sound

Assumes

MonoidWithZero