piCongrLeft — Mathlib

English

Transport dependent functions through an index equivalence; this is the ring-version of Equiv.piCongrLeft.

Русский

Перемещаем зависимые функции через эквивалентность индексов; это кольцевая версия Equiv.piCongrLeft.

LaTeX

$$$$ \\text{RingEquiv.piCongrLeft}(S, e) = (\\text{Equiv.piCongrLeft}'(S, e^{-1})).symm $$$$

Lean4

/-- Transport dependent functions through an equivalence of the base space.

This is `Equiv.piCongrLeft` as a `RingEquiv`. -/
@[simps!]
def piCongrLeft {ι ι' : Type*} (S : ι' → Type*) (e : ι ≃ ι') [∀ i, NonUnitalNonAssocSemiring (S i)] :
    ((i : ι) → S (e i)) ≃+* ((i : ι') → S i) :=
  (RingEquiv.piCongrLeft' S e.symm).symm

Похожие утверждения