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

phiRing_comp

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)

 505def phiRing_comp {A B C : PhiRingObj} (g : PhiRingHom B C) (f : PhiRingHom A B) :
 506    PhiRingHom A C where
 507  map := g.map ∘ f.map

proof body

Definition body.

 508  map_zero := by
 509    change g.map (f.map A.zero) = C.zero
 510    rw [f.map_zero]
 511    exact g.map_zero
 512  map_one := by
 513    change g.map (f.map A.one) = C.one
 514    rw [f.map_one]
 515    exact g.map_one
 516  map_add := by
 517    intro a b
 518    simp [Function.comp, f.map_add, g.map_add]
 519  map_neg := by
 520    intro a
 521    simp [Function.comp, f.map_neg, g.map_neg]
 522  map_mul := by
 523    intro a b
 524    simp [Function.comp, f.map_mul, g.map_mul]
 525  map_phi := by
 526    change g.map (f.map A.phi) = C.phi
 527    rw [f.map_phi]
 528    exact g.map_phi
 529
 530/-- The canonical object of the `PhiRing` category is `ℤ[φ]`. -/

used by (4)

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

depends on (26)

Lean names referenced from this declaration's body.