Expand description
This file contains proofs related to integer multiplication (*
).
These are part of the math standard library.
It’s based on the following file from the Dafny math standard
library:
Source/DafnyStandardLibraries/src/Std/Arithmetic/Mul.dfy
.
That file has the following copyright notice:
/*******************************************************************************
- Original: Copyright (c) Microsoft Corporation * SPDX-License-Identifier: MIT * * Modifications and Extensions: Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT *******************************************************************************/
Functions§
- group_
mul_ basics - group_
mul_ is_ commutative_ and_ distributive - group_
mul_ is_ distributive - group_
mul_ properties - lemma_
mul_ basics - lemma_
mul_ basics_ 1 - lemma_
mul_ basics_ 2 - lemma_
mul_ basics_ 3 - lemma_
mul_ basics_ 4 - lemma_
mul_ by_ zero_ is_ zero - lemma_
mul_ cancels_ negatives - lemma_
mul_ equality_ converse - lemma_
mul_ increases - lemma_
mul_ inequality - lemma_
mul_ inequality_ converse - lemma_
mul_ is_ associative - lemma_
mul_ is_ commutative - lemma_
mul_ is_ distributive_ add - lemma_
mul_ is_ distributive_ add_ other_ way - lemma_
mul_ is_ distributive_ sub - lemma_
mul_ is_ distributive_ sub_ other_ way - lemma_
mul_ is_ mul_ pos - lemma_
mul_ is_ mul_ recursive - lemma_
mul_ left_ inequality - lemma_
mul_ nonnegative - lemma_
mul_ nonzero - lemma_
mul_ ordering - lemma_
mul_ strict_ inequality - lemma_
mul_ strict_ inequality_ converse - lemma_
mul_ strict_ upper_ bound - lemma_
mul_ strictly_ increases - lemma_
mul_ strictly_ positive - lemma_
mul_ unary_ negation - lemma_
mul_ upper_ bound