Theorems · Inductive type · geometry

AffineBasis

Type u₁ →
  (k : Type u₂) →
    {V : Type u₃} →
      (P : Type u₄) → [inst : AddCommGroup V] → [AddTorsor V P] → [inst_2 : Ring k] → [Module k V] → Type (max u₁ u₄)

An affine basis is a family of affine-independent points whose span is the top subspace.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Basis

Cited by

65 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

AddCommGroupAddTorsorRingModule