Closed DyeKuu closed 2 years ago
Note:
The condition i =/= 0, m =/= 0, k =/= 0 should become i =/= m, m =/= k, k =/= i. The Metamath version still enforce the non-zero assumption, which could be deduced by other assumptions.
Note:
The condition i =/= 0, m =/= 0, k =/= 0 should become i =/= m, m =/= k, k =/= i. The Metamath version still enforce the non-zero assumption, which could be deduced by other assumptions.