piLpCongrLeft_symm — Mathlib

English

The inverse of the left congruence is given by applying the left congruence to the inverse index map.

Русский

Обратное к левому конгруентному отображению равносильно применению конгруентности к обратной биекции индексов.

LaTeX

$$$(\text{LinearIsometryEquiv.piLpCongrLeft}(p,\mathbb{K},E,e))^{-1} = \text{LinearIsometryEquiv.piLpCongrLeft}(p,\mathbb{K},E,e^{-1})$$$

Lean4

@[simp]
theorem _root_.LinearIsometryEquiv.piLpCongrLeft_symm (e : ι ≃ ι') :
    (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e).symm = LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm :=
  LinearIsometryEquiv.ext fun z ↦ congr_arg (Equiv.toFun · z) (Equiv.piCongrLeft'_symm _ _)

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