English
A family of linear equivalences indexed by i yields a linear equivalence between pi-types by permuting the index via e: ι' ≃ ι.
Русский
Семейство линейных эквивалентностей, индексируемое по i, образует линейное эквивалентное отображение между пи-типами через перестановку индексов с помощью e: ι' ≃ ι.
LaTeX
$$$((i' : ι') \\to φ(e i')) \\simeq_L[R] (i : ι) \\to φ(i)$$$
Lean4
/-- Combine a family of linear equivalences into a linear equivalence of `pi`-types.
This is `Equiv.piCongrLeft` as a `ContinuousLinearEquiv`.
-/
def piCongrLeft (R : Type*) [Semiring R] {ι ι' : Type*} (φ : ι → Type*) [∀ i, AddCommMonoid (φ i)] [∀ i, Module R (φ i)]
[∀ i, TopologicalSpace (φ i)] (e : ι' ≃ ι) : ((i' : ι') → φ (e i')) ≃L[R] (i : ι) → φ i
where
__ := Homeomorph.piCongrLeft e
__ := LinearEquiv.piCongrLeft R φ e
