General definitions

• Affine space
• Affine function
• Affine subspace
• Barycenter
• Affine span

InstanceAffine groups#

Mathlib states this as AffineEquiv.group.

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

Sources

• Mathlib documentation: AffineEquiv.group
• Source of AffineEquiv.group in Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean
• Mathlib undergraduate list: Affine and Euclidean Geometry › General definitions

MathlibAffineEquiv.group

Uses 2

Statement usesAffine space · Linear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.