English
Affine equivalences between two torsor spaces carry a natural EquivLike structure; equivalently, each affine equivalence determines a bijection between the underlying point sets, and composition/inverses satisfy the usual equivalence laws.
Русский
Аффинные эквивалентности между двумя пространствамиtorsor образуют естественную структуру EquivLike; эквивалентно, каждая аффинная эквивалентность задает биекцию между множествами точек, а композиция и обратные удовлетворяют обычным законам эквивалентности.
LaTeX
$$$\\operatorname{EquivLike}\\big(\\mathrm{AffineEquiv}\\,k\\,P_1\\,P_2\\big)\\;P_1\\;P_2$$$
Lean4
instance equivLike : EquivLike (P₁ ≃ᵃ[k] P₂) P₁ P₂
where
coe f := f.toFun
inv f := f.invFun
left_inv f := f.left_inv
right_inv f := f.right_inv
coe_injective' _ _ h _ := toAffineMap_injective (DFunLike.coe_injective h)
