English
Composition of piCongrRight coordinates matches the piCongrRight of the coordinatewise compositions.
Русский
Составление piCongrRight по координатам совпадает с piCongrRight от координатной композиции.
LaTeX
$$$ (\\mathrm{piCongrRight}\\, e_1).\\mathrm{trans} (\\mathrm{piCongrRight}\\, e_2) = \\mathrm{piCongrRight}\\, (i \\mapsto e_1(i)\\mathrm{.trans}(e_2(i))) $$$
Lean4
/-- 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`.
-/
@[simps apply]
def piCongrRight (e : ∀ i, A₁ i ≃ₐ[R] A₂ i) : (Π i, A₁ i) ≃ₐ[R] Π i, A₂ i :=
{
@RingEquiv.piCongrRight ι A₁ A₂ _ _ fun i ↦
(e i).toRingEquiv with
toFun := fun x j ↦ e j (x j)
invFun := fun x j ↦ (e j).symm (x j)
commutes' := fun r ↦ by
ext i
simp }
