law sum_numel

bendtorch@1.3.0.0 · LAWS.bend:270

import Base
import bendtorch@1.3.0.0/tensor.bend as TT

270# LAW (sum_numel): summing over axis k partitions the elements: a tensor of shape s has exactly size(k) times as many
271# numbers as its sum over axis k, for every shape and every k (past the last axis the size counts as 1).
272law sum_numel:
273  for +s: List<&2, Nat>
274  for +k: Nat
275  {TT.numel(s) == Nat.mul(TT.at1(s, k), TT.numel(TT.remove(s, k))) : Nat}