Revision #1846 → #2353 · back to history
b22c3e2a791c89faf1f32b620fb08ebc36829fbe65612f8a| Field | From #1846 | To #2353 |
|---|---|---|
| mathlib.decl | — | ArithmeticFunction.liouville |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.ArithmeticFunction.Liouville |
| note | The Liouville arithmetic function λ(n) does not appear to be defined in Mathlib (only an unrelated `Liouville` number class exists). | Mathlib defines `ArithmeticFunction.liouville` as the Liouville arithmetic function λ(n). |
| status | not_formalized | formalized |
5d504ea61c3283a9abb7821923b6d00e2308