Theorems · Definition · group theory

MulEquiv.piCongrRight

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

A family of multiplicative equivalences Π j, (Ms j ≃* Ns j) generates a multiplicative equivalence between Π j, Ms j and Π j, Ns j. This is the MulEquiv version of Equiv.piCongrRight, and the dependent version of MulEquiv.arrowCongr.

Defined in

Mathlib.Algebra.Group.Equiv.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

MulMul