Idris2Doc : Algebra.Solver.Ring.Util

Algebra.Solver.Ring.Util

Reexports

import public Syntax.PreorderReasoning

0 p213 : {auto {conArg:808} : Ring a} -> k + (m + n) = m + (k + n): Totality: total
Visibility: export
0 p1324 : {auto {conArg:980} : Ring a} -> (k + l) + (m + n) = (k + m) + (l + n): Totality: total
Visibility: export
0 m1324 : {auto {conArg:1296} : Ring a} -> (k * l) * (m * n) = (k * m) * (l * n): Totality: total
Visibility: export