Module mul

Source
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