Theorems · Inductive type · geometry

AffineEquiv

(k : Type u_1) →
  (P₁ : Type u_2) →
    (P₂ : Type u_3) →
      {V₁ : Type u_4} →
        {V₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [Module k V₁] →
                  [Module k V₂] → [AddTorsor V₁ P₁] → [AddTorsor V₂ 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.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Cited by

191 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 25 definitions · uses no axioms

Assumes

RingAddCommGroupAddCommGroupModuleModuleAddTorsorAddTorsor