~/jendhub

def bc_dim_sym

bendtorch@1.3.0.0 · PROOF.bend:911

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

911# one axis: bc_dim is written as pair(x, y) || pair(y, x), so swapping x and y only swaps the two sides of the ||
912def bc_dim_sym(+x: Nat, +y: Nat, +z: Nat) -> {TT.bc_dim(x, y, z) == TT.bc_dim(y, x, z) : Bool}:
913  or_comm(TT.bc_pair(x, y, z), TT.bc_pair(y, x, z))

Uses (5)

Used by (1)