Mathlib Map

Theorems · Definition · geometry

AffineBasis.toFun

{ι : Type u₁} →
  {k : Type u₂} →
    {V : Type u₃} →
      {P : Type u₄} →
        [inst : AddCommGroup V] →
          [inst_1 : AddTorsor V P] → [inst_2 : Ring k] → [inst_3 : Module k V] → AffineBasis ι k P → ι → P

The underlying family of points. Do NOT use directly. Use the coercion instead.

Defined in
Mathlib.LinearAlgebra.AffineSpace.Basis
Cited by
2 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Assumes
AddCommGroupAddTorsorRingModule
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AffineBasis.tot' · cited by 1AffineBasis.tot'AffineBasis.ind' · cited by 1AffineBasis.ind'Module · cited by 20661ModuleAddCommGroup · cited by 12871AddCommGroupRing · cited by 7463RingAddTorsor · cited by 1657AddTorsorAffineBasis · cited by 65AffineBasisAffineBasis.toFunCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Modulestatement and proof · cited by 20,661
  • AddCommGroupstatement and proof · cited by 12,871
  • Ringstatement and proof · cited by 7,463
  • AddTorsorstatement and proof · cited by 1,657
  • AffineBasisstatement and proof · cited by 65

Cited by2

Results whose statement or proof uses this declaration.