Theorems · Definition · ring theory

NonUnitalRingHom.copy

{α : Type u_2} →
  {β : Type u_3} →
    [inst : NonUnitalNonAssocSemiring α] →
      [inst_1 : NonUnitalNonAssocSemiring β] → (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

2 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring