SumDimsLAWS.sum_dims_keepdim: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/sum_dims_LAWS.bend as SumDimsLAWS
Lines 154-161 of bendtorch-core@0.1.0.0/src/autograd/sum_dims_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims_LAWS.bend&start_line=154&end_line=161

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
import bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend as SumDims

# With keepdim, the sum is exactly reduce_to onto the kept shape.
law sum_dims_keepdim:
  for input: Core.Dynamic
  for +axes: List<&2, U32>
  for +kept: Shape.Shape
  for +dropped: List<&2, U32>
  for planned: {SumDims.plan(Totality.dynamic_shape(input), axes) == Done{SumDims.Plan{kept, dropped}} : Result<&2, &2, SumDims.Error, SumDims.Plan>}
  {SumDims.sum_dims(input, axes, True{}) == as_sum(Reduce.reduce_to(input, kept)) : Core.Dynamic & Result<&2, &1, SumDims.Error, Core.Dynamic>}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=reduce_to
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend&name=plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend&name=sum_checked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims.bend&name=sum_dims
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims_LAWS.bend&name=as_sum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/sum_dims_PROOF.bend&name=kept_as_sum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=dynamic_shape