Theorems · Definition · group theory

AddEquiv.piCongrRight

{η : Type u_16} →
  {Ms : η → Type u_17} →
    {Ns : η → Type u_18} →
      [inst : (j : η) → Add (Ms j)] →
        [inst_1 : (j : η) → Add (Ns j)] → ((j : η) → Ms j ≃+ Ns j) → ((j : η) → Ms j) ≃+ ((j : η) → Ns j)

A family of additive equivalences Π j, (Ms j ≃+ Ns j) generates an additive equivalence between Π j, Ms j and Π j, Ns j. This is the AddEquiv version of Equiv.piCongrRight, and the dependent version of AddEquiv.arrowCongr.

Defined in

Mathlib.Algebra.Group.Equiv.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

AddAdd