law mul_mul_mul_comm

bend-mathlib@0.8.1.0 · nat.bend:2174

import Base

2174# Four-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d).
2175law mul_mul_mul_comm:
2176  for a: Nat
2177  for b: Nat
2178  for c: Nat
2179  for d: Nat
2180  {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}