piCongrRight_symm — Mathlib

English

Define a linear equivalence transporting dependent functions across an equivalence of index types.

Русский

Определяем линейное эквивалентное отображение, перемещающее зависимые функции через эквиваленцию индексов.

LaTeX

$$$$\\text{piCongrLeft'}(e) : ((i' : ι') \\to φ i') \\simeq_l ((i : ι') \\to φ (i)). $$$$

Lean4

@[simp]
theorem piCongrRight_symm (e : (i : ι) → φ i ≃ₗ[R] ψ i) : (piCongrRight e).symm = piCongrRight fun i => (e i).symm :=
  rfl

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