Theorems · Definition · ring theory

NonUnitalRingHom.op

{R : Type u_2} →
  {S : Type u_3} →
    [inst : NonUnitalNonAssocSemiring R] → [inst_1 : NonUnitalNonAssocSemiring S] → (R →ₙ+* S) ≃ (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ)

A non-unital ring hom R →ₙ+* S can equivalently be viewed as a non-unital ring hom Rᵐᵒᵖ →+* Sᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Defined in

Mathlib.Algebra.Ring.Opposite

Cited by

2 results in Mathlib

Foundations

Depth 22 from the axioms · uses Quot.sound

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring