Revision #1726 → #2257 · back to history
modifiedEven and odd integersa5459a41dc82
| Field | From #1726 | To #2257 |
|---|
| mathlib.decl | Odd | Even |
| mathlib.module | Mathlib.Algebra.Ring.Parity | Mathlib.Algebra.Group.Even |
| note | `Even` is defined in `Mathlib.Algebra.Group.Even` as `∃ r, a = r + r` and `Odd a := ∃ k, a = 2 * k + 1` in `Mathlib.Algebra.Ring.Parity`. | `Even a := ∃ r, a = r + r` is defined in `Mathlib.Algebra.Group.Even`; `Odd a := ∃ k, a = 2 * k + 1` (in `Mathlib.Algebra.Ring.Parity`) formalizes the not-divisible-by-2 side. |
| provenance | ai | ai-moderated |
modifiedAverage number of divisorsf3a0c9a906a3
| Field | From #1726 | To #2257 |
|---|
| anchor.snippet | where [MATH] is Euler–Mascheroni constant | Euler–Mascheroni constant |
| provenance | ai | ai-moderated |
modifiedDivisibility closed under suma5d94f2187a3
| Field | From #1726 | To #2257 |
|---|
| anchor.snippet | However, if [MATH] and [MATH] then [MATH] does not always hold | holds, as does |
| note | `dvd_add : a ∣ b → a ∣ c → a ∣ b + c` formalizes that if `a` divides `b` and `c` then `a` divides `b + c`. | `dvd_add : a ∣ b → a ∣ c → a ∣ b + c` formalizes that if `a` divides `b` and `c` then `a` divides `b + c`; the parallel rule for differences is `dvd_sub`. |
| provenance | ai | ai-moderated |
modifiedGreatest common divisor (as meet)a7e8a816cceb
| Field | From #1726 | To #2257 |
|---|
| mathlib.module | Mathlib.Data.Nat.GCD.Basic | Init.Data.Nat.Gcd |
modifiedLeast common multiple (as join)c7f41a9d5161
| Field | From #1726 | To #2257 |
|---|
| mathlib.module | Mathlib.Data.Nat.GCD.Basic | Init.Data.Nat.Lcm |
modifiedCoprime numbers9b087a4c83e6
| Field | From #1726 | To #2257 |
|---|
| mathlib.module | Mathlib.Data.Nat.GCD.Basic | Init.Data.Nat.Coprime |
addedDivisibility in a ring3338261eb3a3
addedSet of positive divisors4be675124deb