pith. machine review for the scientific record. sign in
structure definition def or abbrev

Hom

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  31structure Hom (A B : PeanoObject) where
  32  toFun : A.carrier → B.carrier
  33  map_zero : toFun A.zero = B.zero
  34  map_step : ∀ x : A.carrier, toFun (A.step x) = B.step (toFun x)
  35
  36namespace Hom
  37
  38instance (A B : PeanoObject) : CoeFun (Hom A B) (fun _ => A.carrier → B.carrier) where
  39  coe f := f.toFun

proof body

Definition body.

  40
  41/-- Identity homomorphism. -/

used by (10)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.