Lean4
/-- 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`.
-/
@[to_additive (attr := simps apply) /-- 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`. -/
]
def piCongrRight {η : Type*} {Ms Ns : η → Type*} [∀ j, Mul (Ms j)] [∀ j, Mul (Ns j)] (es : ∀ j, Ms j ≃* Ns j) :
(∀ j, Ms j) ≃* ∀ j, Ns j :=
{ Equiv.piCongrRight fun j => (es j).toEquiv with toFun := fun x j => es j (x j),
invFun := fun x j => (es j).symm (x j), map_mul' := fun x y => funext fun j => map_mul (es j) (x j) (y j) }
