English
Combine a family of linear equivalences into a linear equivalence on Pi-types.
Русский
Объединение семейства линейных эквивалентностей в линейную эквивалентность на произведении.
LaTeX
$$$$\\pi\\mathrm{CongrRight}(e) : ((i : ι) \\to φ_i) \\simeq_l ((i : ι) \\to ψ_i),$$ where $e_i : φ_i \\simeq_l ψ_i$.$$
Lean4
/-- Combine a family of linear equivalences into a linear equivalence of `pi`-types.
This is `Equiv.piCongrRight` as a `LinearEquiv` -/
def piCongrRight (e : (i : ι) → φ i ≃ₗ[R] ψ i) : ((i : ι) → φ i) ≃ₗ[R] (i : ι) → ψ i :=
{
AddEquiv.piCongrRight fun j => (e
j).toAddEquiv with
toFun := fun f i => e i (f i)
invFun := fun f i => (e i).symm (f i)
map_smul' := fun c f => by ext; simp }
