Theorems · Definition · ring theory

NonUnitalRingHom.fromOpposite

{R : Type u_2} →
  {S : Type u_3} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] → (f : R →ₙ+* S) → (∀ (x y : R), Commute (f x) (f y)) → Rᵐᵒᵖ →ₙ+* S

A non-unital ring homomorphism f : R →ₙ* S such that f x commutes with f y for all x, y defines a non-unital ring homomorphism from Rᵐᵒᵖ.

Defined in

Mathlib.Algebra.Ring.Opposite

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring