Theorems · Definition · ring theory

RingHom.copy

{α : Type u_2} →
  {β : Type u_3} →
    {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → (f : α →+* β) → (f' : α → β) → f' = ⇑f → α →+* β

Copy of a RingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

3 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms