Revision #1535 → #2803 · back to history
modifiedIrrational numberd676bde8feb0
| Field | From #1535 | To #2803 |
|---|
| note | `Irrational x` is defined as `x ∉ Set.range ((↑) : ℚ → ℝ)` with companion `irrational_iff_ne_rational`. | `Irrational x` is defined at line 37 of `Mathlib/NumberTheory/Real/Irrational.lean` as `x ∉ Set.range ((↑) : ℚ → ℝ)`. |
modifiedRepeating decimal as geometric series82cd26a5c00b
| Field | From #1535 | To #2803 |
|---|
| note | Geometric series sums (`tsum_geometric_of_lt_one`, etc.) are formalized but not specialised to summing a repeating digit block to a fraction. | Geometric series sums (`tsum_geometric_of_lt_one`) are formalized but not specialised to summing a repeating digit block to a fraction. |
added0.999... = 1ace6c3c0044a
addedFermat's little theorem for base 10 mod p304f25875509
addedCyclic permutation of digits (rotation)6a86bdb5853e
addedMultiplicative order of b modulo qb6c2d7683251
addedCarmichael's theorem (λ(n) bounds order)302812b260aa