symm_linear — Mathlib

English

Same mathematical content as the inverse of an affine equivalence has its linear part inverted; the alias keeps identical meaning though it is deprecated.

Русский

Та же самая математика: обратное аффинного эквивалента имеет обращение линейной части; это устаревшая запись.

LaTeX

$$$ (e^{\mathrm{toEquiv}})^{-1} = e^{\mathrm{symm}} $$$

Lean4

@[deprecated "use instead `linear_symm`, in the reverse direction" (since := "2025-06-08")]
theorem symm_linear (e : P₁ ≃ᵃ[k] P₂) : e.linear.symm = e.symm.linear :=
  rfl

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