linear_symm — Mathlib

English

For an affine equivalence e, the linear part of its inverse equals the inverse of the linear part of e; equivalently, the linear component of e^{-1} is the inverse linear map of the linear component of e.

Русский

Для аффинного равенства e линейная часть обратного отображения равняется обратному линейному отображению линейной части e.

LaTeX

$$$ (e^{-1}).linear = (e.linear)^{-1} $$$

Lean4

@[simp]
theorem linear_symm (e : P₁ ≃ᵃ[k] P₂) : e.symm.linear = e.linear.symm :=
  rfl

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