Theorems · Definition · ring theory

RingEquiv.toRingHom

{R : Type u_4} → {S : Type u_5} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → R ≃+* S → R →+* S

Reinterpret a ring equivalence as a ring homomorphism.

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

150 results in Mathlib

Foundations

Depth 21 from the axioms, rests on 154 definitions · uses Quot.sound

Assumes

NonAssocSemiringNonAssocSemiring