symm — Mathlib

English

The linear part of mk' equals the given linear equivalence e'.

Русский

Линейная часть mk' равна заданной линейной эквивалентности e'.

LaTeX

$$$\text{linear}((\mathrm{mk'}\,e\,e'\,p\,h)) = e'$$$

Lean4

/-- Inverse of an affine equivalence as an affine equivalence. -/
@[symm]
def symm (e : P₁ ≃ᵃ[k] P₂) : P₂ ≃ᵃ[k] P₁ where
  toEquiv := e.toEquiv.symm
  linear := e.linear.symm
  map_vadd' p
    v :=
    e.toEquiv.symm.apply_eq_iff_eq_symm_apply.2 <| by
      rw [Equiv.symm_symm, e.map_vadd' ((Equiv.symm e.toEquiv) p) ((LinearEquiv.symm e.linear) v),
        LinearEquiv.apply_symm_apply, Equiv.apply_symm_apply]

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