bend-mathlib
Search uses release 0.8.1.0 · 1,126 definitions
Definitions (1,126)
- law double_div_two_add_mod_twoTwice the half plus the parity is the number: double (n / 2) + n % 2 = n.
- law add_le_add_iff_rightAdding the same amount on the right does not change the order test: a <= b tests as a + k <= b + k.
- law add_left_cancel_iffAdding the same amount on the left does not change the equality test: a = b tests as k + a = k + b.
- law add_right_cancel_iffAdding the same amount on the right does not change the equality test: a = b tests as a + k = b + k.
- law sub_add_commSubtracting from the left summand commutes with adding the right one: k <= n implies (n + m) - k = (n - k) + m.
- law le_min_of_le_of_leA lower bound of both b and c is a lower bound of their minimum: a <= b and a <= c imply a <= min b c.
- law max_le_of_le_of_leAn upper bound of both a and b bounds their maximum: a <= c and b <= c imply max a b <= c.
- law mul_twoMultiplying n by two gives n + n.
- law pow_twoSquaring n gives n times n.
- law min_le_maxThe minimum of two numbers is at most their maximum.
- law double_injDoubling is injective: double a = double b implies a = b.
- def internal_double_ne_succ_double
- law double_ne_succ_doubleAn even number is not odd: double a differs from 1 + double b.
- law two_pow_succTwo to a successor power is double the power: 2^(n+1) = double (2^n).
- law add_zero_symZero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.
- law zero_add_symZero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.
- law add_succ_symAdding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
- law succ_add_symAdding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
- law add_comm_symAddition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
- law add_assoc_symAddition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
- law add_left_comm_symLeft commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
- law add_right_comm_symRight commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
- law add_add_add_comm_symFour-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
- law mul_zero_symZero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
- law zero_mul_symZero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
- law mul_one_symOne is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.
- law one_mul_symOne is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.
- law mul_succ_symMultiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.
- law succ_mul_symMultiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
- law mul_comm_symMultiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
- law add_mul_symMultiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
- law mul_add_symMultiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
- law mul_assoc_symMultiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
- law sub_zero_symSubtracting zero changes nothing: n - 0 = n, reversed to rewrite toward the simple side.
- law zero_sub_symTruncated subtraction from zero is zero: 0 - n = 0, reversed to rewrite toward the simple side.
- law sub_self_symA natural minus itself is zero: n - n = 0, reversed to rewrite toward the simple side.
- law succ_sub_succ_symSubtracting successors: (n + 1) - (m + 1) = n - m, reversed to rewrite toward the simple side.
- law add_sub_cancel_symAdding then subtracting m cancels: (n + m) - m = n, reversed to rewrite toward the simple side.
- law add_sub_cancel_left_symAdding then subtracting n cancels: (n + m) - n = m, reversed to rewrite toward the simple side.
- law sub_sub_symSubtracting twice is subtracting the sum: (n - m) - k = n - (m + k), reversed to rewrite toward the simple side.
- law div_mod_eq_symThe division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a, reversed to rewrite toward the simple side.
- law add_div_left_symAdding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b), reversed to rewrite toward the simple side.
- law le_div_iff_mul_le_symA quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a, reversed to rewrite toward the simple side.
- law min_comm_symMinimum is commutative, reversed to rewrite toward the simple side.
- law max_comm_symMaximum is commutative, reversed to rewrite toward the simple side.
- law min_self_symThe minimum of a natural and itself is itself, reversed to rewrite toward the simple side.
- law max_self_symThe maximum of a natural and itself is itself, reversed to rewrite toward the simple side.
- law min_zero_symThe minimum with zero is zero: min(a, 0) = 0, reversed to rewrite toward the simple side.
- law zero_min_symThe minimum with zero is zero: min(0, a) = 0, reversed to rewrite toward the simple side.
- law max_zero_symZero is an identity for maximum: max(a, 0) = a, reversed to rewrite toward the simple side.
- law zero_max_symZero is an identity for maximum: max(0, a) = a, reversed to rewrite toward the simple side.
- law min_assoc_symMinimum is associative, reversed to rewrite toward the simple side.
- law max_assoc_symMaximum is associative, reversed to rewrite toward the simple side.
- law min_add_max_symThe minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b, reversed to rewrite toward the simple side.
- law pow_zero_symAny natural to the power zero is one, reversed to rewrite toward the simple side.
- law pow_succ_symA power with a successor exponent: a^(n+1) = a * a^n, reversed to rewrite toward the simple side.
- law pow_one_symAny natural to the power one is itself, reversed to rewrite toward the simple side.
- law one_pow_symOne to any power is one, reversed to rewrite toward the simple side.
- law pow_add_symExponents add under multiplication: a^(m+n) = a^m * a^n, reversed to rewrite toward the simple side.
- law double_eq_add_symDoubling is adding a natural to itself, reversed to rewrite toward the simple side.
- law is_eq_refl_symEvery natural tests equal to itself, reversed to rewrite toward the simple side.
- law is_eq_comm_symThe equality test is symmetric, reversed to rewrite toward the simple side.
- law is_ge_eq_is_le_symA >= b tests the same as b <= a, reversed to rewrite toward the simple side.
- law is_gt_eq_is_lt_symA > b tests the same as b < a, reversed to rewrite toward the simple side.
- law is_lt_eq_succ_le_symA < b tests the same as a + 1 <= b, reversed to rewrite toward the simple side.
- law not_is_le_symNot (a <= b) tests the same as b < a, reversed to rewrite toward the simple side.
- law not_is_lt_symNot (a < b) tests the same as b <= a, reversed to rewrite toward the simple side.
- law add_le_add_iff_left_symAdding the same amount on the left does not change the order test: a <= b tests as k + a <= k + b, reversed to rewrite toward the simple side.
- law le_and_le_sub_iff_add_le_symA sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both, reversed to rewrite toward the simple side.
- law min_le_iff_symThe minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c, reversed to rewrite toward the simple side.
- law lt_max_iff_symThe maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c, reversed to rewrite toward the simple side.
- law lt_sub_iff_add_lt_symComparing against a difference is comparing the sum: a < c - b tests as b + a < c, reversed to rewrite toward the simple side.
- law zero_div_symZero divided by anything is zero: 0 / b = 0, reversed to rewrite toward the simple side.
- law zero_mod_symZero modulo anything is zero: 0 % b = 0, reversed to rewrite toward the simple side.
- law div_one_symDividing by one changes nothing: a / 1 = a, reversed to rewrite toward the simple side.
- law mod_one_symAny natural modulo one is zero: a % 1 = 0, reversed to rewrite toward the simple side.
- law mod_self_symA natural modulo itself is zero: n % n = 0, reversed to rewrite toward the simple side.
- law div_self_symA positive natural divided by itself is one: (1 + b) / (1 + b) = 1, reversed to rewrite toward the simple side.
- law mod_mod_symTaking a remainder twice is taking it once: (a % n) % n = a % n, reversed to rewrite toward the simple side.
- law add_mod_left_symAdding the divisor does not change the remainder: (b + a) % b = a % b, reversed to rewrite toward the simple side.
- law mul_div_cancel_symMultiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a, reversed to rewrite toward the simple side.
- law mul_div_cancel_left_symMultiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a, reversed to rewrite toward the simple side.
- law mul_mod_left_symA multiple of b leaves no remainder modulo b: (a * b) % b = 0, reversed to rewrite toward the simple side.
- law mul_mod_right_symA multiple of a leaves no remainder modulo a: (a * b) % a = 0, reversed to rewrite toward the simple side.
- law mod_add_div_symThe remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a, reversed to rewrite toward the simple side.
- law mul_left_comm_symLeft commutativity of multiplication: a * (b * c) = b * (a * c), reversed to rewrite toward the simple side.
- law mul_right_comm_symRight commutativity of multiplication: (a * b) * c = (a * c) * b, reversed to rewrite toward the simple side.
- law mul_mul_mul_comm_symFour-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d), reversed to rewrite toward the simple side.
- law zero_pow_symZero to a positive power is zero: 0^(n+1) = 0, reversed to rewrite toward the simple side.
- law mul_pow_symA power of a product is the product of the powers: (a * b)^n = a^n * b^n, reversed to rewrite toward the simple side.
- law pow_mul_symExponents multiply under repeated powers: a^(m * n) = (a^m)^n, reversed to rewrite toward the simple side.
- law add_sub_add_left_symA common left summand cancels in a difference: (k + n) - (k + m) = n - m, reversed to rewrite toward the simple side.
- law add_sub_add_right_symA common right summand cancels in a difference: (n + k) - (m + k) = n - m, reversed to rewrite toward the simple side.
- law sub_mul_symMultiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k, reversed to rewrite toward the simple side.
- law mul_sub_symMultiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k, reversed to rewrite toward the simple side.
- law le_min_symA number is at most the minimum exactly when it is at most both: a <= min b c tests as a <= b and a <= c (Mathlib's le_min_iff; the implication is le_min_of_le_of_le), reversed to rewrite toward the simple side.
- law max_le_symThe maximum is at most c exactly when both arguments are: max a b <= c tests as a <= c and b <= c (Mathlib's max_le_iff; the implication is max_le_of_le_of_le), reversed to rewrite toward the simple side.
- law lt_succ_iff_symBelow a successor means at most: m < n + 1 tests as m <= n, reversed to rewrite toward the simple side.
- law le_iff_lt_or_eq_symAt most means below or equal: a <= b tests as a < b or a = b, reversed to rewrite toward the simple side.
- law lt_iff_le_and_ne_symBelow means at most and different: a < b tests as a <= b and not a = b, reversed to rewrite toward the simple side.