Coordinates of basis vectors

The coordinate of a colour basis vector is the equality indicator: the coordinate calculus closes on basis input.

theorem RS.coordOf_evenBasisVec {k ℓ n : ℕ} (c : MixedColouring k ℓ n) (hc : c.IsEven) (c' : MixedColouring k ℓ n) : coordOf (evenBasisVec ⟨c, hc⟩) c' = if c' = c then 1 else 0

The basis coordinate indicator.

theorem RS.evenBasisVec_zeroArity {k ℓ : ℕ} (x : { c : MixedColouring k ℓ 0 // c.IsEven }) : evenBasisVec x = 1

The arity-zero basis vector is the unit scalar.