Int.gcd_ne_one_iff_gcd_mul_right_ne_one
theorem Int.gcd_ne_one_iff_gcd_mul_right_ne_one :
∀ {a : ℤ} {m n : ℕ}, a.gcd (↑m * ↑n) ≠ 1 ↔ a.gcd ↑m ≠ 1 ∨ a.gcd ↑n ≠ 1
This theorem states that for any integer `a` and natural numbers `m` and `n`, if the greatest common divisor (`gcd`) of `a` and the product of `m` and `n` is not 1, then the `gcd` of `a` with either `m` or `n` must not be 1. This is a statement about divisibility properties in number theory.
More concisely: If the greatest common divisor of an integer `a` with `m` \* `n` is not 1, then the greatest common divisor of `a` with `m` or `n` is also not 1.
|
Int.abs_eq_normalize
theorem Int.abs_eq_normalize : ∀ (z : ℤ), |z| = normalize z
This theorem states that for any integer `z`, the absolute value of `z` is equal to the normalization of `z`. In other words, when we take an integer `z`, its absolute value (denoted as `|z|`) is identical to the result of applying the `normalize` function to `z`. This function is defined in a way that it chooses an element of each associate class, multiplying it by `normUnit`. The `normalize` function operates within the context of a `CancelCommMonoidWithZero` and a `NormalizationMonoid`.
More concisely: For any integer `z`, the absolute value `|z|` is equal to the result of normalizing `z` using the `normalize` function. (This statement assumes the `normalize` function satisfies the properties of a `NormalizationMonoid` in the given context.)
|
Nat.factors_eq
theorem Nat.factors_eq : ∀ {n : ℕ}, UniqueFactorizationMonoid.normalizedFactors n = ↑n.factors
The theorem `Nat.factors_eq` states that for every natural number 'n', the multiset of prime factors determined noncomputably (via the `UniqueFactorizationMonoid.normalizedFactors` function) is equal to the coercion of the list of prime factors of 'n' (obtained by the `Nat.factors` function). In other words, both methods for obtaining the prime factorization of a natural number 'n' yield the same result, despite one being a multiset and the other being a list.
More concisely: For every natural number n, the multiset of prime factors obtained noncomputably is equal to the coercion of the list of prime factors of n.
|
Int.gcd_eq_one_iff_coprime
theorem Int.gcd_eq_one_iff_coprime : ∀ {a b : ℤ}, a.gcd b = 1 ↔ IsCoprime a b
The theorem `Int.gcd_eq_one_iff_coprime` establishes a bi-directional relationship between two integers `a` and `b` having a greatest common divisor equal to 1 and being coprime. In other words, for any two integers `a` and `b`, they are coprime (there exist two numbers such that their linear combination equals 1) if and only if the greatest common divisor of `a` and `b` is 1.
More concisely: Two integers `a` and `b` are coprime if and only if their greatest common divisor equals 1.
|
Int.gcd_eq_natAbs
theorem Int.gcd_eq_natAbs : ∀ {a b : ℤ}, a.gcd b = a.natAbs.gcd b.natAbs
This theorem states that for any two integers `a` and `b`, the greatest common divisor (gcd) of `a` and `b` can be computed as the gcd of the absolute values of `a` and `b`. The absolute value of an integer is found using the `Int.natAbs` function, which returns the natural number corresponding to the integer's absolute value. In other words, the gcd of any two integers is equal to the gcd of their absolute values.
More concisely: For any integers a and b, |a|gcd a b = |b|gcd a b, where |a| denotes the absolute value of integer a.
|
Int.normalize_of_nonneg
theorem Int.normalize_of_nonneg : ∀ {z : ℤ}, 0 ≤ z → normalize z = z
This theorem states that for any integer `z` that is non-negative (i.e., greater than or equal to zero), normalizing `z` results in `z` itself. Here, the normalization is done using the `normalize` function, which chooses an element from each associate class by multiplying by the normalizing unit (`normUnit`).
More concisely: For any non-negative integer `z`, normalizing `z` using Lean's `normalize` function returns `z`.
|
induction_on_primes
theorem induction_on_primes : ∀ {P : ℕ → Prop}, P 0 → P 1 → (∀ (p a : ℕ), p.Prime → P a → P (p * a)) → ∀ (n : ℕ), P n
The theorem `induction_on_primes` states that for any property `P`, which maps natural numbers to a proposition, if `P` holds true for `0` and `1`, and if `P` is true for a natural number `a` and a prime number `p`, then `P` continues to hold true for the product of `p` and `a`, then `P` is true for all natural numbers `n`. This is a form of mathematical induction tailored specifically for prime numbers and their multiples.
More concisely: If a property holds for 0 and 1, and for any prime number p and natural number a with Pa, then Pa \* p implies Pn for all natural numbers n.
|