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]