Tensor.flat_numel: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/tensor.bend as Tensor
Lines 456-458 of bendtorch@1.3.0.0/tensor.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/tensor.bend&start_line=456&end_line=458

import Base
import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL

# n * 1 == n, so a shape and its flattening hold the same count
def flat_numel(+s: List<&2, Nat>) -> {numel(s) == numel([numel(s)]) : Nat}:
  Equal.sym(Nat, Nat.mul(numel(s), 1n), numel(s), NL.mul_one_r(numel(s)))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=mul_one_r
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=numel