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

import Base

# the mean over axis k: the sum divided by the axis' size
def mean_axis(+s: List<&2, Nat>, +k: Nat, x: Tensor<s>) -> TP<s, remove(s, k)>:
  tp_div(s, remove(s, k), n_f32(at1(s, k)), sum_axis(s, k, x))

Uses (9):
  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=bendtorch@1.3.0.0/tensor.bend&name=TP
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=at1
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=n_f32
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=remove
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=sum_axis
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=tp_div