vstd
In vstd::
arithmetic::
div_
mod
Functions
group_div_basics
group_fundamental_div_mod_converse
group_mod_basics
group_mod_properties
is_mod_equivalent
lemma_add_mod_noop
lemma_add_mod_noop_right
lemma_basic_div
lemma_basic_div_specific_divisor
lemma_breakdown
lemma_div_basics
lemma_div_basics_1
lemma_div_basics_2
lemma_div_basics_3
lemma_div_basics_4
lemma_div_basics_5
lemma_div_by_multiple
lemma_div_by_multiple_is_strongly_ordered
lemma_div_by_self
lemma_div_decreases
lemma_div_denominator
lemma_div_is_div_recursive
lemma_div_is_ordered
lemma_div_is_ordered_by_denominator
lemma_div_is_strictly_smaller
lemma_div_minus_one
lemma_div_multiples_vanish
lemma_div_multiples_vanish_fancy
lemma_div_multiples_vanish_quotient
lemma_div_non_zero
lemma_div_nonincreasing
lemma_div_of0
lemma_div_plus_one
lemma_div_pos_is_pos
lemma_dividing_sums
lemma_fundamental_div_mod
lemma_fundamental_div_mod_converse
lemma_fundamental_div_mod_converse_div
lemma_fundamental_div_mod_converse_mod
lemma_hoist_over_denominator
lemma_indistinguishable_quotients
lemma_mod_add_multiples_vanish
lemma_mod_adds
lemma_mod_bound
lemma_mod_breakdown
lemma_mod_decreases
lemma_mod_division_less_than_divisor
lemma_mod_equivalence
lemma_mod_is_mod_recursive
lemma_mod_is_zero
lemma_mod_mod
lemma_mod_mul_equivalent
lemma_mod_multiples_basic
lemma_mod_multiples_vanish
lemma_mod_neg_neg
lemma_mod_ordering
lemma_mod_pos_bound
lemma_mod_self_0
lemma_mod_sub_multiples_vanish
lemma_mod_subtraction
lemma_mod_twice
lemma_mul_hoist_inequality
lemma_mul_mod_noop
lemma_mul_mod_noop_general
lemma_mul_mod_noop_left
lemma_mul_mod_noop_right
lemma_multiply_divide_le
lemma_multiply_divide_lt
lemma_part_bound1
lemma_part_bound2
lemma_remainder
lemma_remainder_lower
lemma_remainder_upper
lemma_round_down
lemma_small_div_converse
lemma_small_mod
lemma_sub_mod_noop
lemma_sub_mod_noop_right
lemma_truncate_middle
?
Settings
Function
vstd
::
arithmetic
::
div_mod
::
group_mod_properties
Copy item path
source
·
[
−
]
pub
broadcast group
fn group_mod_properties()
Expand description
broadcast group