English
Transport dependent functions through an index equivalence. There is a ring isomorphism between ((i:ι) → R i) and ((i:ι') → R (e.symm i)) whose underlying equivalence is Equiv.piCongrLeft' R e and whose ring-structure maps are trivial (rfl).
Русский
Перемещаем зависимые функции через эквивалентность индексов. Существует кольцевой эквивалент между ((i:ι) → R i) и ((i:ι') → R (e.symm i)), чья база-эквиваленция задается Equiv.piCongrLeft' R e и чьи операции сложения и умножения совпадают с соответствующими дефолнными значениями.
LaTeX
$$$$\\left((i: ι) \\to R i\\right) \\cong+* \\left((i: ι') \\to R (e.symm\\, i)\\right)$$$$
Lean4
/-- Transport dependent functions through an equivalence of the base space.
This is `Equiv.piCongrLeft'` as a `RingEquiv`. -/
@[simps!]
def piCongrLeft' {ι ι' : Type*} (R : ι → Type*) (e : ι ≃ ι') [∀ i, NonUnitalNonAssocSemiring (R i)] :
((i : ι) → R i) ≃+* ((i : ι') → R (e.symm i))
where
toEquiv := Equiv.piCongrLeft' R e
map_mul' _ _ := rfl
map_add' _ _ := rfl
