def cv_mul

bend-kit-collections@0.1.4.1 · nat_order.bend:197

import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder

import Base

197def cv_mul(k: Nat, +A: Nat, +p: Lin, +v: Vs, +eA: {A == F(p, v) : Nat})
198  -> {Nat.mul(k, A) == F(lsc(k, p), v) : Nat}:
199  match k:
200    case 0n:
201      sy(F(L{0n, 0n, 0n, 0n, 0n}, v), 0n, F0(v))
202    case 1n+ +j:
203      cv_add(A, Nat.mul(j, A), p, lsc(j, p), v, eA, cv_mul(j, A, p, v, eA))

Uses (9)

Used by (26)