Theorems · Theorem · ring theory

NonUnitalRingHom.coe_copy

∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring