Revision #3172 → #3664 · back to history
d79681a97c74| Field | From #3172 | To #3664 |
|---|---|---|
| note | Mathlib has Real.transcendental_pi but no derivation of the impossibility of squaring the circle as a constructibility result. | Mathlib has the transcendence of π but no derivation of the impossibility of squaring the circle as a constructibility result. |
caf6ca10bd164a7054275a15197cbbe43b6b17f44ae58b65