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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] extends Equiv : Type (max (max (max u_2 u_3) u_4) u_5)

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

An affine equivalence 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 «term_≃ᵃ[_]_» : Lean.TrailingParserDescr

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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] : Function.Injective AffineEquiv.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] : EquivLike (P₁ ≃ᵃ[k] P₂) P₁ P₂

instance AffineEquiv.instCoeFunAffineEquivForAll {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] : CoeFun (P₁ ≃ᵃ[k] P₂) fun x => P₁ → P₂

instance AffineEquiv.instCoeOutAffineEquivEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : ↑e.toEquiv = ↑e

instance AffineEquiv.instCoeAffineEquivAffineMap {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {e' : P₁ ≃ᵃ[k] P₂} (h : ∀ (x : P₁), ↑e x = ↑e' x) : e = e'

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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] : Function.Injective FunLike.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] : Function.Injective AffineEquiv.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), ↑e p' = ↑e' (p' -ᵥ p) +ᵥ ↑e p) : ↑(AffineEquiv.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁) (h : ∀ (p' : P₁), ↑e p' = ↑e' (p' -ᵥ p) +ᵥ ↑e p) : (AffineEquiv.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : P₂ ≃ᵃ[k] P₁

Inverse of an affine equivalence as an affine equivalence.

@[simp]

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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : e.symm = (AffineEquiv.symm e).toEquiv

@[simp]

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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : LinearEquiv.symm e.linear = (AffineEquiv.symm e).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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : Function.Injective ↑e

@[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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ↑φ) (a : P₁) : ↑(AffineEquiv.ofBijective hφ) a = ↑φ a

@[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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ↑φ) : (AffineEquiv.ofBijective hφ).linear = LinearEquiv.ofBijective φ.linear (_ : Function.Bijective ↑φ.linear)

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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ↑φ) : P₁ ≃ᵃ[k] P₂

Bijective affine maps are affine isomorphisms.

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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ↑φ) : (AffineEquiv.symm (AffineEquiv.ofBijective hφ)).toEquiv = (Equiv.ofBijective (↑φ) hφ).symm

@[simp]

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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₂) : ↑e (↑(AffineEquiv.symm e) 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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₁) : ↑(AffineEquiv.symm e) (↑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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {p₁ : P₁} {p₂ : (fun a => P₂) p₁} : ↑e p₁ = p₂ ↔ p₁ = ↑(AffineEquiv.symm e) 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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) {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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) : ↑(AffineEquiv.symm f) '' 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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₁) : ↑(AffineEquiv.symm f) ⁻¹' 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₁] : ↑(AffineEquiv.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₁] : ↑(AffineEquiv.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₁) : ↑(AffineEquiv.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₁] : (AffineEquiv.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₁] : (AffineEquiv.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₁] : AffineEquiv.symm (AffineEquiv.refl k P₁) = AffineEquiv.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : ↑(AffineEquiv.trans e 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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : ↑(AffineEquiv.trans e e') = AffineMap.comp ↑e' ↑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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) (p : P₁) : ↑(AffineEquiv.trans e 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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₂ ≃ᵃ[k] P₃) (e₃ : P₃ ≃ᵃ[k] P₄) : AffineEquiv.trans (AffineEquiv.trans e₁ e₂) e₃ = AffineEquiv.trans e₁ (AffineEquiv.trans e₂ 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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : AffineEquiv.trans e (AffineEquiv.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : AffineEquiv.trans (AffineEquiv.refl k P₁) 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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : AffineEquiv.trans e (AffineEquiv.symm e) = AffineEquiv.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) : AffineEquiv.trans (AffineEquiv.symm e) e = AffineEquiv.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (a : P₁) (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 = AffineEquiv.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 : P₁ ≃ᵃ[k] P₁) (e' : P₁ ≃ᵃ[k] P₁) : e * e' = AffineEquiv.trans e' 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 : P₁ ≃ᵃ[k] P₁) (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⁻¹ = AffineEquiv.symm e

@[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₁) : ↑AffineEquiv.linearHom self = self.linear

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.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₁) : ↑(↑AffineEquiv.equivUnitsAffineMap e) = ↑e

@[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₁)ˣ) : (↑(MulEquiv.symm AffineEquiv.equivUnitsAffineMap) u).linear = ↑(LinearMap.GeneralLinearGroup.generalLinearEquiv k V₁) (↑(Units.map AffineMap.linearHom) u)

@[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₁) : ↑(↑(MulEquiv.symm AffineEquiv.equivUnitsAffineMap) u) 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₁) : ↑(↑(MulEquiv.symm AffineEquiv.equivUnitsAffineMap) u) a = ↑↑u a

@[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₁) : Equiv.invFun (↑(MulEquiv.symm AffineEquiv.equivUnitsAffineMap) u).toEquiv a = ↑↑u⁻¹ a

@[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₁) : ↑(AffineEquiv.symm (↑(MulEquiv.symm AffineEquiv.equivUnitsAffineMap) u)) a = ↑↑u⁻¹ a

@[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₁) : ↑(↑AffineEquiv.equivUnitsAffineMap e)⁻¹ = ↑(AffineEquiv.symm e)

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.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₁) : (AffineEquiv.vaddConst k b).linear = LinearEquiv.refl k 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' : P₁) : ↑(AffineEquiv.symm (AffineEquiv.vaddConst k b)) 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₁) : ↑(AffineEquiv.vaddConst k b) v = v +ᵥ b

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.

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₁) : ↑(AffineEquiv.constVSub k p) = (fun x x_1 => x -ᵥ x_1) p

@[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₁) : ↑(AffineEquiv.symm (AffineEquiv.constVSub k p)) = fun v => -v +ᵥ p

@[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₁), ↑(AffineEquiv.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₁) : (AffineEquiv.constVAdd k P₁ v).linear = LinearEquiv.refl k V₁

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_zero (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] : AffineEquiv.constVAdd k P₁ 0 = AffineEquiv.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 : V₁) (w : V₁) : AffineEquiv.constVAdd k P₁ (v + w) = AffineEquiv.trans (AffineEquiv.constVAdd k P₁ w) (AffineEquiv.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₁) : AffineEquiv.symm (AffineEquiv.constVAdd k P₁ v) = AffineEquiv.constVAdd k P₁ (-v)

@[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₁) : ↑(AffineEquiv.constVAddHom k P₁) v = AffineEquiv.constVAdd k P₁ (↑Multiplicative.toAdd 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.

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₁) : AffineEquiv.constVAdd k P₁ (n • v) = AffineEquiv.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₁) : AffineEquiv.constVAdd k P₁ (z • v) = AffineEquiv.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ˣ) : ↑(↑(AffineEquiv.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ˣ) : ↑(AffineEquiv.symm (↑(AffineEquiv.homothetyUnitsMulHom p) t)) = ↑(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) : AffineEquiv.toAffineMap ∘ ↑(AffineEquiv.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.

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 : P₁) (y : P₁) : ↑(AffineEquiv.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₁) : AffineEquiv.symm (AffineEquiv.pointReflection k x) = AffineEquiv.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₁) : (AffineEquiv.pointReflection k x).toEquiv = Equiv.pointReflection x

@[simp]

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₁) : ↑(AffineEquiv.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 ↑(AffineEquiv.pointReflection k x)

theorem AffineEquiv.pointReflection_fixed_iff_of_injective_bit0 (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {x : P₁} {y : P₁} (h : Function.Injective bit0) : ↑(AffineEquiv.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_bit0 (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 bit0) (y : P₁) : Function.Injective fun x => ↑(AffineEquiv.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 => ↑(AffineEquiv.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 : P₁} {y : P₁} : ↑(AffineEquiv.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₁] [Module k V₁] [AddCommGroup 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₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂] (e : V₁ ≃ₗ[k] V₂) : ↑(LinearEquiv.toAffineEquiv e) = ↑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' : V₁) (p : P₁) (c : k) : ↑(AffineMap.lineMap v v') c +ᵥ p = ↑(AffineMap.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₁) (p₃ : P₁) (c : k) : ↑(AffineMap.lineMap p₁ p₂) c -ᵥ p₃ = ↑(AffineMap.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₁) (p₃ : P₁) (c : k) : p₁ -ᵥ ↑(AffineMap.lineMap p₂ p₃) c = ↑(AffineMap.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₂ : P₁) (c : k) : v +ᵥ ↑(AffineMap.lineMap p₁ p₂) c = ↑(AffineMap.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 : P₁) : ↑(AffineMap.homothety c (-1)) p = ↑(AffineEquiv.pointReflection R' c) p