Theorems · Theorem · order theory

OrderMonoidWithZeroHom.mk.inj

∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {inst_2 : MulZeroOneClass α}
  {inst_3 : MulZeroOneClass β} {toMonoidWithZeroHom : α →*₀ β} {monotone' : Monotone (↑toMonoidWithZeroHom).toFun}
  {toMonoidWithZeroHom_1 : α →*₀ β} {monotone'_1 : Monotone (↑toMonoidWithZeroHom_1).toFun},
  { toMonoidWithZeroHom := toMonoidWithZeroHom, monotone' := monotone' } =
      { toMonoidWithZeroHom := toMonoidWithZeroHom_1, monotone' := monotone'_1 } →
    toMonoidWithZeroHom = toMonoidWithZeroHom_1

Defined in

Mathlib.Algebra.Order.Hom.MonoidWithZero

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms