Affine equivalences

In this file we define AffineEquiv k P₁ P₂ (notation: P₁ ≃ᵃ[k] P₂) to be the type of affine equivalences between P₁ and P₂, i.e., equivalences such that both forward and inverse maps are affine maps.

We define the following equivalences:

• AffineEquiv.refl k P: the identity map as an AffineEquiv;

• e.symm: the inverse map of an AffineEquiv as an AffineEquiv;

• e.trans e': composition of two AffineEquivs; note that the order follows mathlib's CategoryTheory convention (apply e, then e'), not the convention used in function composition and compositions of bundled morphisms.

We equip AffineEquiv k P P with a Group structure with multiplication corresponding to composition in AffineEquiv.group.

Tags

affine space, affine equivalence

structure AffineEquiv (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_4} {V₂ : Type u_5} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] extends P₁ ≃ P₂ : Type (max (max (max u_2 u_3) u_4) u_5)

An affine equivalence, denoted P₁ ≃ᵃ[k] P₂, is an equivalence between affine spaces such that both forward and inverse maps are affine.

We define it using an Equiv for the map and a LinearEquiv for the linear part in order to allow affine equivalences with good definitional equalities.

• toFun : P₁ → P₂
• invFun : P₂ → P₁
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• linear : V₁ ≃ₗ[k] V₂
• map_vadd' (p : P₁) (v : V₁) : self.toEquiv (v +ᵥ p) = self.linear v +ᵥ self.toEquiv p

def «term_≃ᵃ[_]_» : Lean.TrailingParserDescr

An affine equivalence, denoted P₁ ≃ᵃ[k] P₂, is an equivalence between affine spaces such that both forward and inverse maps are affine.

We define it using an Equiv for the map and a LinearEquiv for the linear part in order to allow affine equivalences with good definitional equalities.

def AffineEquiv.toAffineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : P₁ →ᵃ[k] P₂

Reinterpret an AffineEquiv as an AffineMap.

@[simp]

theorem AffineEquiv.toAffineMap_mk {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ ≃ P₂) (f' : V₁ ≃ₗ[k] V₂) (h : ∀ (p : P₁) (v : V₁), f (v +ᵥ p) = f' v +ᵥ f p) : ↑{ toEquiv := f, linear := f', map_vadd' := h } = { toFun := ⇑f, linear := ↑f', map_vadd' := h }

@[simp]

theorem AffineEquiv.linear_toAffineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : (↑e).linear = ↑e.linear

theorem AffineEquiv.toAffineMap_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] : Function.Injective toAffineMap

@[simp]

theorem AffineEquiv.toAffineMap_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} : ↑e = ↑e' ↔ e = e'

instance AffineEquiv.equivLike {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] : EquivLike (P₁ ≃ᵃ[k] P₂) P₁ P₂

instance AffineEquiv.instCoeOutEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] : CoeOut (P₁ ≃ᵃ[k] P₂) (P₁ ≃ P₂)

@[simp]

theorem AffineEquiv.map_vadd {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) : e (v +ᵥ p) = e.linear v +ᵥ e p

@[simp]

theorem AffineEquiv.coe_toEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : ⇑e.toEquiv = ⇑e

instance AffineEquiv.instCoeAffineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] : Coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂)

@[simp]

theorem AffineEquiv.coe_toAffineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : ⇑↑e = ⇑e

@[simp]

theorem AffineEquiv.coe_coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : ⇑↑e = ⇑e

@[simp]

theorem AffineEquiv.coe_linear {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : (↑e).linear = ↑e.linear

theorem AffineEquiv.ext {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} (h : ∀ (x : P₁), e x = e' x) : e = e'

theorem AffineEquiv.ext_iff {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} : e = e' ↔ ∀ (x : P₁), e x = e' x

theorem AffineEquiv.coeFn_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] : Function.Injective DFunLike.coe

theorem AffineEquiv.coeFn_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} : ⇑e = ⇑e' ↔ e = e'

theorem AffineEquiv.toEquiv_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] : Function.Injective toEquiv

@[simp]

theorem AffineEquiv.toEquiv_inj {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂} : e.toEquiv = e'.toEquiv ↔ e = e'

@[simp]

theorem AffineEquiv.coe_mk {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = e' v +ᵥ e p) : ⇑{ toEquiv := e, linear := e', map_vadd' := h } = ⇑e

def AffineEquiv.mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ → P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) : P₁ ≃ᵃ[k] P₂

Construct an affine equivalence by verifying the relation between the map and its linear part at one base point. Namely, this function takes a map e : P₁ → P₂, a linear equivalence e' : V₁ ≃ₗ[k] V₂, and a point p such that for any other point p' we have e p' = e' (p' -ᵥ p) +ᵥ e p.

@[simp]

theorem AffineEquiv.coe_mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) : ⇑(mk' (⇑e) e' p h) = ⇑e

@[simp]

theorem AffineEquiv.linear_mk' {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p) : (mk' (⇑e) e' p h).linear = e'

def AffineEquiv.symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : P₂ ≃ᵃ[k] P₁

Inverse of an affine equivalence as an affine equivalence.

@[simp]

theorem AffineEquiv.toEquiv_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : e.symm.toEquiv = e.symm

@[deprecated "use instead `toEquiv_symm`, in the reverse direction" (since := "2025-06-08")]

theorem AffineEquiv.symm_toEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : e.symm = e.symm.toEquiv

@[simp]

theorem AffineEquiv.coe_symm_toEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : ⇑e.symm = ⇑e.symm

@[simp]

theorem AffineEquiv.linear_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : e.symm.linear = e.linear.symm

@[deprecated "use instead `linear_symm`, in the reverse direction" (since := "2025-06-08")]

theorem AffineEquiv.symm_linear {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : e.linear.symm = e.symm.linear

def AffineEquiv.Simps.apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : P₁ → P₂

See Note [custom simps projection]

def AffineEquiv.Simps.symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : P₂ → P₁

See Note [custom simps projection]

theorem AffineEquiv.bijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : Function.Bijective ⇑e

theorem AffineEquiv.surjective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : Function.Surjective ⇑e

theorem AffineEquiv.injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : Function.Injective ⇑e

noncomputable def AffineEquiv.ofBijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) : P₁ ≃ᵃ[k] P₂

Bijective affine maps are affine isomorphisms.

@[simp]

theorem AffineEquiv.linear_ofBijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) : (ofBijective hφ).linear = LinearEquiv.ofBijective φ.linear ⋯

@[simp]

theorem AffineEquiv.ofBijective_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) (a : P₁) : (ofBijective hφ) a = φ a

theorem AffineEquiv.ofBijective.symm_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ) : (ofBijective hφ).symm.toEquiv = (Equiv.ofBijective (⇑φ) hφ).symm

theorem AffineEquiv.range_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : Set.range ⇑e = Set.univ

@[simp]

theorem AffineEquiv.apply_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₂) : e (e.symm p) = p

@[simp]

theorem AffineEquiv.symm_apply_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) : e.symm (e p) = p

theorem AffineEquiv.apply_eq_iff_eq_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ : P₁} {p₂ : P₂} : e p₁ = p₂ ↔ p₁ = e.symm p₂

theorem AffineEquiv.apply_eq_iff_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ p₂ : P₁} : e p₁ = e p₂ ↔ p₁ = p₂

@[simp]

theorem AffineEquiv.image_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) : ⇑f.symm '' s = ⇑f ⁻¹' s

@[simp]

theorem AffineEquiv.preimage_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₁) : ⇑f.symm ⁻¹' s = ⇑f '' s

def AffineEquiv.refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : P₁ ≃ᵃ[k] P₁

Identity map as an AffineEquiv.

@[simp]

theorem AffineEquiv.coe_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : ⇑(refl k P₁) = id

@[simp]

theorem AffineEquiv.coe_refl_to_affineMap (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : ↑(refl k P₁) = AffineMap.id k P₁

@[simp]

theorem AffineEquiv.refl_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) : (refl k P₁) x = x

@[simp]

theorem AffineEquiv.toEquiv_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : (refl k P₁).toEquiv = Equiv.refl P₁

@[simp]

theorem AffineEquiv.linear_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : (refl k P₁).linear = LinearEquiv.refl k V₁

@[simp]

theorem AffineEquiv.symm_refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : (refl k P₁).symm = refl k P₁

def AffineEquiv.trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : P₁ ≃ᵃ[k] P₃

Composition of two AffineEquivalences, applied left to right.

@[simp]

theorem AffineEquiv.coe_trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : ⇑(e.trans e') = ⇑e' ∘ ⇑e

@[simp]

theorem AffineEquiv.coe_trans_to_affineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : ↑(e.trans e') = (↑e').comp ↑e

@[simp]

theorem AffineEquiv.trans_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V₁] [Module k V₂] [Module k V₃] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) (p : P₁) : (e.trans e') p = e' (e p)

theorem AffineEquiv.trans_assoc {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} {V₄ : Type u_9} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [AddCommGroup V₄] [Module k V₁] [Module k V₂] [Module k V₃] [Module k V₄] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] [AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₂ ≃ᵃ[k] P₃) (e₃ : P₃ ≃ᵃ[k] P₄) : (e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃)

@[simp]

theorem AffineEquiv.trans_refl {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : e.trans (refl k P₂) = e

@[simp]

theorem AffineEquiv.refl_trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : (refl k P₁).trans e = e

@[simp]

theorem AffineEquiv.self_trans_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : e.trans e.symm = refl k P₁

@[simp]

theorem AffineEquiv.symm_trans_self {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : e.symm.trans e = refl k P₂

@[simp]

theorem AffineEquiv.apply_lineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] [AddTorsor V₁ P₁] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k) : e ((AffineMap.lineMap a b) c) = (AffineMap.lineMap (e a) (e b)) c

instance AffineEquiv.group {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : Group (P₁ ≃ᵃ[k] P₁)

theorem AffineEquiv.one_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : 1 = refl k P₁

@[simp]

theorem AffineEquiv.coe_one {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : ⇑1 = id

theorem AffineEquiv.mul_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (e e' : P₁ ≃ᵃ[k] P₁) : e * e' = e'.trans e

@[simp]

theorem AffineEquiv.coe_mul {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (e e' : P₁ ≃ᵃ[k] P₁) : ⇑(e * e') = ⇑e ∘ ⇑e'

theorem AffineEquiv.inv_def {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) : e⁻¹ = e.symm

def AffineEquiv.linearHom {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : (P₁ ≃ᵃ[k] P₁) →* V₁ ≃ₗ[k] V₁

AffineEquiv.linear on automorphisms is a MonoidHom.

@[simp]

theorem AffineEquiv.linearHom_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (self : P₁ ≃ᵃ[k] P₁) : linearHom self = self.linear

def AffineEquiv.equivUnitsAffineMap {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : (P₁ ≃ᵃ[k] P₁) ≃* (P₁ →ᵃ[k] P₁)ˣ

The group of AffineEquivs are equivalent to the group of units of AffineMap.

This is the affine version of LinearMap.GeneralLinearGroup.generalLinearEquiv.

@[simp]

theorem AffineEquiv.val_inv_equivUnitsAffineMap_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) : ↑(equivUnitsAffineMap e)⁻¹ = ↑e.symm

@[simp]

theorem AffineEquiv.equivUnitsAffineMap_symm_apply_invFun {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) : (equivUnitsAffineMap.symm u).invFun a = ↑u⁻¹ a

@[simp]

theorem AffineEquiv.equivUnitsAffineMap_symm_apply_toFun {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) : (equivUnitsAffineMap.symm u) a = ↑u a

@[simp]

theorem AffineEquiv.equivUnitsAffineMap_symm_apply_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) : (equivUnitsAffineMap.symm u) a = ↑u a

@[simp]

theorem AffineEquiv.linear_equivUnitsAffineMap_symm_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) : (equivUnitsAffineMap.symm u).linear = (LinearMap.GeneralLinearGroup.generalLinearEquiv k V₁) ((Units.map AffineMap.linearHom) u)

@[simp]

theorem AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁) : (equivUnitsAffineMap.symm u).symm a = ↑u⁻¹ a

@[simp]

theorem AffineEquiv.val_equivUnitsAffineMap_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁) : ↑(equivUnitsAffineMap e) = ↑e

def AffineEquiv.vaddConst (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (b : P₁) : V₁ ≃ᵃ[k] P₁

The map v ↦ v +ᵥ b as an affine equivalence between a module V and an affine space P with tangent space V.

@[simp]

theorem AffineEquiv.vaddConst_symm_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (b p' : P₁) : (vaddConst k b).symm p' = p' -ᵥ b

@[simp]

theorem AffineEquiv.vaddConst_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (b : P₁) (v : V₁) : (vaddConst k b) v = v +ᵥ b

@[simp]

theorem AffineEquiv.linear_vaddConst (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (b : P₁) : (vaddConst k b).linear = LinearEquiv.refl k V₁

def AffineEquiv.constVSub (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p : P₁) : P₁ ≃ᵃ[k] V₁

p' ↦ p -ᵥ p' as an equivalence.

@[simp]

theorem AffineEquiv.coe_constVSub (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p : P₁) : ⇑(constVSub k p) = fun (x : P₁) => p -ᵥ x

@[simp]

theorem AffineEquiv.coe_constVSub_symm (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p : P₁) : ⇑(constVSub k p).symm = fun (v : V₁) => -v +ᵥ p

def AffineEquiv.constVAdd (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) : P₁ ≃ᵃ[k] P₁

The map p ↦ v +ᵥ p as an affine automorphism of an affine space.

Note that there is no need for an AffineMap.constVAdd as it is always an equivalence. This is roughly to DistribMulAction.toLinearEquiv as +ᵥ is to •.

@[simp]

theorem AffineEquiv.constVAdd_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) (x✝ : P₁) : (constVAdd k P₁ v) x✝ = v +ᵥ x✝

@[simp]

theorem AffineEquiv.linear_constVAdd (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) : (constVAdd k P₁ v).linear = LinearEquiv.refl k V₁

@[simp]

theorem AffineEquiv.constVAdd_zero (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : constVAdd k P₁ 0 = refl k P₁

@[simp]

theorem AffineEquiv.constVAdd_add (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v w : V₁) : constVAdd k P₁ (v + w) = (constVAdd k P₁ w).trans (constVAdd k P₁ v)

@[simp]

theorem AffineEquiv.constVAdd_symm (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) : (constVAdd k P₁ v).symm = constVAdd k P₁ (-v)

def AffineEquiv.constVAddHom (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : Multiplicative V₁ →* P₁ ≃ᵃ[k] P₁

A more bundled version of AffineEquiv.constVAdd.

@[simp]

theorem AffineEquiv.constVAddHom_apply (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : Multiplicative V₁) : (constVAddHom k P₁) v = constVAdd k P₁ (Multiplicative.toAdd v)

theorem AffineEquiv.constVAdd_nsmul (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (n : ℕ) (v : V₁) : constVAdd k P₁ (n • v) = constVAdd k P₁ v ^ n

theorem AffineEquiv.constVAdd_zsmul (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (z : ℤ) (v : V₁) : constVAdd k P₁ (z • v) = constVAdd k P₁ v ^ z

def AffineEquiv.homothetyUnitsMulHom {R : Type u_10} {V : Type u_11} {P : Type u_12} [CommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p : P) : Rˣ →* P ≃ᵃ[R] P

Fixing a point in affine space, homothety about this point gives a group homomorphism from (the centre of) the units of the scalars into the group of affine equivalences.

@[simp]

theorem AffineEquiv.coe_homothetyUnitsMulHom_apply {R : Type u_10} {V : Type u_11} {P : Type u_12} [CommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p : P) (t : Rˣ) : ⇑((homothetyUnitsMulHom p) t) = ⇑(AffineMap.homothety p ↑t)

@[simp]

theorem AffineEquiv.coe_homothetyUnitsMulHom_apply_symm {R : Type u_10} {V : Type u_11} {P : Type u_12} [CommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p : P) (t : Rˣ) : ⇑((homothetyUnitsMulHom p) t).symm = ⇑(AffineMap.homothety p ↑t⁻¹)

@[simp]

theorem AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe {R : Type u_10} {V : Type u_11} {P : Type u_12} [CommRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (p : P) : toAffineMap ∘ ⇑(homothetyUnitsMulHom p) = ⇑(AffineMap.homothetyHom p) ∘ Units.val

def AffineEquiv.pointReflection (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) : P₁ ≃ᵃ[k] P₁

Point reflection in x as a permutation.

@[simp]

theorem AffineEquiv.pointReflection_apply_eq_equivPointReflection_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x y : P₁) : (pointReflection k x) y = (Equiv.pointReflection x) y

theorem AffineEquiv.pointReflection_apply (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x y : P₁) : (pointReflection k x) y = (x -ᵥ y) +ᵥ x

@[simp]

theorem AffineEquiv.pointReflection_symm (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) : (pointReflection k x).symm = pointReflection k x

@[simp]

theorem AffineEquiv.toEquiv_pointReflection (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) : (pointReflection k x).toEquiv = Equiv.pointReflection x

theorem AffineEquiv.pointReflection_self (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) : (pointReflection k x) x = x

theorem AffineEquiv.pointReflection_involutive (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (x : P₁) : Function.Involutive ⇑(pointReflection k x)

theorem AffineEquiv.pointReflection_fixed_iff_of_injective_two_nsmul (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {x y : P₁} (h : Function.Injective fun (x : V₁) => 2 • x) : (pointReflection k x) y = y ↔ y = x

x is the only fixed point of pointReflection x. This lemma requires x + x = y + y ↔ x = y. There is no typeclass to use here, so we add it as an explicit argument.

theorem AffineEquiv.injective_pointReflection_left_of_injective_two_nsmul (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (h : Function.Injective fun (x : V₁) => 2 • x) (y : P₁) : Function.Injective fun (x : P₁) => (pointReflection k x) y

theorem AffineEquiv.injective_pointReflection_left_of_module (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [Invertible 2] (y : P₁) : Function.Injective fun (x : P₁) => (pointReflection k x) y

theorem AffineEquiv.pointReflection_fixed_iff_of_module (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [Invertible 2] {x y : P₁} : (pointReflection k x) y = y ↔ y = x

def LinearEquiv.toAffineEquiv {k : Type u_1} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] (e : V₁ ≃ₗ[k] V₂) : V₁ ≃ᵃ[k] V₂

Interpret a linear equivalence between modules as an affine equivalence.

@[simp]

theorem LinearEquiv.coe_toAffineEquiv {k : Type u_1} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [AddCommGroup V₂] [Module k V₁] [Module k V₂] (e : V₁ ≃ₗ[k] V₂) : ⇑e.toAffineEquiv = ⇑e

theorem AffineMap.lineMap_vadd {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v v' : V₁) (p : P₁) (c : k) : (lineMap v v') c +ᵥ p = (lineMap (v +ᵥ p) (v' +ᵥ p)) c

theorem AffineMap.lineMap_vsub {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p₁ p₂ p₃ : P₁) (c : k) : (lineMap p₁ p₂) c -ᵥ p₃ = (lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)) c

theorem AffineMap.vsub_lineMap {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (p₁ p₂ p₃ : P₁) (c : k) : p₁ -ᵥ (lineMap p₂ p₃) c = (lineMap (p₁ -ᵥ p₂) (p₁ -ᵥ p₃)) c

theorem AffineMap.vadd_lineMap {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (v : V₁) (p₁ p₂ : P₁) (c : k) : v +ᵥ (lineMap p₁ p₂) c = (lineMap (v +ᵥ p₁) (v +ᵥ p₂)) c

theorem AffineMap.homothety_neg_one_apply {P₁ : Type u_2} {V₁ : Type u_6} [AddCommGroup V₁] [AddTorsor V₁ P₁] {R' : Type u_10} [CommRing R'] [Module R' V₁] (c p : P₁) : (homothety c (-1)) p = (AffineEquiv.pointReflection R' c) p