safe-tensor-0.2.1.0: Dependently typed tensor algebra

Math.Tensor.Basic.Delta

Description

Definitions of Kronecker deltas $$\delta^{a}_{\hphantom ab}$$ (identity automorphisms) for arbitrary vector spaces.

Synopsis

# Kronecker delta

delta :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v. ('['('VSpace id n, 'ConCov (a :| '[]) (b :| '[]))] ~ r, TailR (TailR r) ~ '[], Sane (TailR r) ~ 'True, SingI n, Num v) => Tensor r v Source #

The Kronecker delta $$\delta^a_{\hphantom ab}$$ for a given VSpace id n with contravariant index label a and covariant index label b.

delta' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v. (KnownNat n, Num v, '['('VSpace id n, 'ConCov (a :| '[]) (b :| '[]))] ~ r, TailR (TailR r) ~ '[], Sane (TailR r) ~ 'True) => Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v Source #

The Kronecker delta $$\delta^a_{\hphantom ab}$$ for a given VSpace id n with contravariant index label a and covariant index label b. Labels and dimension are passed explicitly as singletons.

The Kronecker delta $$\delta^a_{\hphantom ab}$$ for a given VSpace id n with contravariant index label a and covariant index label b. Labels and dimension are passed as values. Result is existentially quantified.