Documentation

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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:

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)

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.

Instances For
    theorem AffineEquiv.map_vadd' {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₂] (self : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) :
    self.toEquiv (v +ᵥ p) = self.linear v +ᵥ self.toEquiv p

    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      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.

      Equations
      • e = { toFun := e.toFun, linear := e.linear, map_vadd' := }
      Instances For
        @[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₂
        Equations
        • AffineEquiv.equivLike = { coe := fun (f : P₁ ≃ᵃ[k] P₂) => f.toFun, inv := fun (f : P₁ ≃ᵃ[k] P₂) => f.invFun, left_inv := , right_inv := , coe_injective' := }
        instance AffineEquiv.instCoeFunForall {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₁ ≃ᵃ[k] P₂) => P₁P₂
        Equations
        • AffineEquiv.instCoeFunForall = DFunLike.hasCoeToFun
        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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] :
        CoeOut (P₁ ≃ᵃ[k] P₂) (P₁ P₂)
        Equations
        • AffineEquiv.instCoeOutEquiv = { coe := AffineEquiv.toEquiv }
        @[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.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] :
        Coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂)
        Equations
        • AffineEquiv.instCoeAffineMap = { coe := AffineEquiv.toAffineMap }
        @[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_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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {e : P₁ ≃ᵃ[k] P₂} {e' : P₁ ≃ᵃ[k] P₂} :
        e = e' ∀ (x : P₁), e x = e' x
        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 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₁] [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.

        Equations
        • AffineEquiv.mk' e e' p h = { toFun := e, invFun := fun (q' : P₂) => e'.symm (q' -ᵥ e p) +ᵥ p, left_inv := , right_inv := , linear := e', map_vadd' := }
        Instances For
          @[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.

          Equations
          • e.symm = { toEquiv := e.symm, linear := e.linear.symm, map_vadd' := }
          Instances For
            @[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 = e.symm.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₂) :
            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₁] [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]

            Equations
            Instances For
              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]

              Equations
              Instances For
                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₂) :
                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₂) :
                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₂) :
                @[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 φ) :
                @[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₁) :
                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.

                Equations
                Instances For
                  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.ofBijective ).symm.toEquiv = (Equiv.ofBijective (⇑φ) ).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 (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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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₁] [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₂) :
                  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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [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.

                  Equations
                  Instances For
                    @[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.refl k P₁).symm = 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.

                    Equations
                    • e.trans e' = { toEquiv := e.trans e'.toEquiv, linear := e.linear.trans e'.linear, map_vadd' := }
                    Instances For
                      @[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₃) :
                      (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₁] [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.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₁] [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₁) :
                      (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₁] [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₄) :
                      (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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
                      e.trans (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.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₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) :
                      e.trans e.symm = 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₂) :
                      e.symm.trans 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₁)
                      Equations
                      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₁] :
                      @[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' = 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 : 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⁻¹ = e.symm
                      @[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.

                      Equations
                      • AffineEquiv.linearHom = { toFun := AffineEquiv.linear, map_one' := , map_mul' := }
                      Instances For
                        @[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)⁻¹ = e.symm
                        @[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₁) :
                        (AffineEquiv.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₁) :
                        (AffineEquiv.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₁)ˣ) :
                        (AffineEquiv.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₁) :
                        (AffineEquiv.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₁) :
                        (AffineEquiv.equivUnitsAffineMap e) = e
                        @[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₁) :
                        (AffineEquiv.equivUnitsAffineMap.symm u).invFun a = u⁻¹ a
                        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.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[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₁) :
                          @[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.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₁) :
                          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.

                          Equations
                          Instances For
                            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.

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

                              Equations
                              Instances For
                                @[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₁] :
                                @[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.constVAdd k P₁ w).trans (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₁) :
                                @[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.

                                Equations
                                Instances For
                                  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₁) :
                                  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₁) :
                                  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) :

                                  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.

                                  Equations
                                  Instances For
                                    @[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ˣ) :
                                    @[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ˣ) :
                                    @[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.

                                    Equations
                                    Instances For
                                      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₁) :
                                      @[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₁) :
                                      @[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₁) :
                                      @[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₁) :
                                      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₁) :
                                      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 fun (x : V₁) => 2 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 fun (x : V₁) => 2 x) (y : P₁) :
                                      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₁) :
                                      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₁} :
                                      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.

                                      Equations
                                      • e.toAffineEquiv = { toEquiv := e.toEquiv, linear := e, map_vadd' := }
                                      Instances For
                                        @[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₂) :
                                        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' : 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₁) :