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

PhiRingHom

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)

 485structure PhiRingHom (A B : PhiRingObj) where
 486  map : A.Carrier → B.Carrier
 487  map_zero : map A.zero = B.zero
 488  map_one : map A.one = B.one
 489  map_add : ∀ a b, map (A.add a b) = B.add (map a) (map b)
 490  map_neg : ∀ a, map (A.neg a) = B.neg (map a)
 491  map_mul : ∀ a b, map (A.mul a b) = B.mul (map a) (map b)
 492  map_phi : map A.phi = B.phi
 493
 494/-- Identity morphism in `PhiRing`. -/

used by (6)

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

depends on (19)

Lean names referenced from this declaration's body.