Theorems · Definition · ring theory

RingEquiv.piCongrRight

{ι : Type u_7} →
  {R : ι → Type u_8} →
    {S : ι → Type u_9} →
      [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)] →
        [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (S i)] →
          ((i : ι) → R i ≃+* S i) → ((i : ι) → R i) ≃+* ((i : ι) → S i)

A family of ring isomorphisms ∀ j, (R j ≃+* S j) generates a ring isomorphisms between ∀ j, R j and ∀ j, S j. This is the RingEquiv version of Equiv.piCongrRight, and the dependent version of RingEquiv.arrowCongr.

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

5 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring