Theorems · Theorem · group theory

MonoidWithZeroHom.coe_mk

∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : ZeroHom α β)
  (h1 : f.toFun 1 = 1) (hmul : ∀ (x y : α), f.toFun (x * y) = f.toFun x * f.toFun y),
  ⇑{ toZeroHom := f, map_one' := h1, map_mul' := hmul } = ⇑f

Defined in

Mathlib.Algebra.GroupWithZero.Hom

Cited by

7 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

MulZeroOneClassMulZeroOneClass