Theorems · Definition · ring theory

AlgEquiv.piCongrRight

{R : Type u_3} →
  {ι : Type u_4} →
    {A₁ : ι → Type u_5} →
      {A₂ : ι → Type u_6} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → Semiring (A₁ i)] →
            [inst_2 : (i : ι) → Semiring (A₂ i)] →
              [inst_3 : (i : ι) → Algebra R (A₁ i)] →
                [inst_4 : (i : ι) → Algebra R (A₂ i)] →
                  ((i : ι) → A₁ i ≃ₐ[R] A₂ i) → ((i : ι) → A₁ i) ≃ₐ[R] (i : ι) → A₂ i

A family of algebra equivalences ∀ i, (A₁ i ≃ₐ A₂ i) generates a multiplicative equivalence between Π i, A₁ i and Π i, A₂ i. This is the AlgEquiv version of Equiv.piCongrRight, and the dependent version of AlgEquiv.arrowCongr.

Defined in

Mathlib.Algebra.Algebra.Pi

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringAlgebraAlgebra