Revision #1546 → #1793 · back to history
modifiedRoman numerals (definition)12df82961fa1
| Field | From #1546 | To #1793 |
|---|
| note | Mathlib has no Roman numeral system; a grep for "roman" returns no results. | Grep for "roman" in Mathlib/ returns no files; Roman numeral system is not formalized. |
modifiedAdditive principleb73a7945d8ae
| Field | From #1546 | To #1793 |
|---|
| note | No Roman numeral encoding or its additive principle is defined in Mathlib. | No Roman numeral encoding exists in Mathlib, so its additive principle is unformalized. |
modifiedSeven symbol lettersc32cf793ae23
| Field | From #1546 | To #1793 |
|---|
| note | The seven Roman symbol letters are not represented anywhere in Mathlib. | The seven Roman symbol letters (I, V, X, L, C, D, M) are not represented in Mathlib. |
modifiedXXVII = 272e7d28d9a675
| Field | From #1546 | To #1793 |
|---|
| note | No Roman numeral parsing exists to give XXVII = 27 in Mathlib. | No Roman numeral parsing exists in Mathlib to give XXVII = 27. |
addedExamples 39, 246, 789, 2421137239e10f5b
addedApostrophus IↃ = 500, CIↃ = 1,00081529be2d4d7
addedVinculum IV = 4,000, XXV = 25,00067f97562d7f3
addedNon-positional numeral system8d709622e6eb