Revision #2846 → #3829 · back to history
modifiedCoprime integers5975535a526a
| Field | From #2846 | To #3829 |
|---|
| mathlib.module | Mathlib.Data.Nat.GCD.Basic | Init.Data.Nat.Coprime |
modifiedNotation for coprimalitye119e7be2531
| Field | From #2846 | To #3829 |
|---|
| mathlib.module | Mathlib.Data.Nat.GCD.Basic | Init.Data.Nat.Coprime |
modified1 and -1 coprime with every integer227339dc2a01
| Field | From #2846 | To #3829 |
|---|
| mathlib.module | Mathlib.Data.Nat.GCD.Basic | Init.Data.Nat.Coprime |
modifiedEquivalent conditions for coprimalityafd5eea43ea2
| Field | From #2846 | To #3829 |
|---|
| mathlib.module | Mathlib.RingTheory.Int.Basic | Mathlib.RingTheory.Coprime.Lemmas |
addedBézout's identity for coprime integers0a90e7f71d60
addedMultiplicative inverse mod a00783c08d19d
addedChinese remainder theorem for two coprime moduli15454763b756
addedlcm equals product when coprimebcc424f9452c
addedProduct of two coprimes is coprime8067c810808e
modifiedEuclid's lemma (prime form)bdf780756591
| Field | From #2846 | To #3829 |
|---|
| label | Euclid's lemma | Euclid's lemma (prime form) |
| mathlib.decl | IsCoprime.dvd_of_dvd_mul_right | Nat.Prime.dvd_mul |
| mathlib.module | Mathlib.RingTheory.Coprime.Basic | Mathlib.Data.Nat.Prime.Defs |
| note | Formalized as `IsCoprime.dvd_of_dvd_mul_right` (and the Int version in `Mathlib.Data.Int.GCD` is explicitly labeled `Euclid's lemma`). | Euclid's lemma in prime form: `p.Prime → (p ∣ m * n ↔ p ∣ m ∨ p ∣ n)`. Also `Prime.dvd_or_dvd` in general commutative monoids. |
| provenance | ai | ai-moderated |
modifiedGeneralization of Euclid's lemma6a7d2e1928b9
| Field | From #2846 | To #3829 |
|---|
| note | This is the same statement as Euclid's lemma above and is proved as `IsCoprime.dvd_of_dvd_mul_right`/`_left`. | `IsCoprime.dvd_of_dvd_mul_right : IsCoprime k n → k ∣ m * n → k ∣ m` (and `_left`). |
addedFermat numbers are pairwise coprime3551674cd131
addedBasel problem ζ(2) = π²/6a38a03367b81
addedProduct of coprime ideals equals intersection159022ac0643