Anne's blog post on dedekind domains and class number #9
Conversation
| Alternatively, we can parse ((algebraic number) theory) as the area of mathematics studying [algebraic](https://leanprover-community.github.io/mathlib_docs/ring_theory/algebraic.html#is_algebraic) numbers, those satisfying a polynomial equation $f(\alpha) = 0$ for some nonzero polynomial $f$ with rational coefficients. | ||
| Algebraic numbers are found in [*number fields*](https://leanprover-community.github.io/mathlib_docs/number_theory/number_field.html#number_field), which are finite extensions of the field of rational numbers, | ||
| or equivalently fields generated by adjoining an algebraic element $\alpha$ to $\Q$ (by virtue of the [primitive element theorem](https://leanprover-community.github.io/mathlib_docs/field_theory/primitive_element.html#field.exists_primitive_element)). | ||
| Much like $\Q$ contains the integers $\Z$ as a subring, a number field $K$ contains a [*ring of integers*](https://leanprover-community.github.io/mathlib_docs/number_theory/number_field.html#number_field.ring_of_integers) $O_K$, |
There was a problem hiding this comment.
I wonder if we want to use the find style links like docs# on zulip uses, to prevent these links breaking when they inevitably get moved between files.
There was a problem hiding this comment.
I agree with Eric's point, however I do think it's really cool that, like Wikipedia or nlab, we can talk about concepts and then directly link to them, so I absolutely think we should have some sort of link here.
There was a problem hiding this comment.
On the other hand, find might not help too much if we rename the defs as well. Perhaps the best solution is some form of link-integrity linter?
There was a problem hiding this comment.
Ideally we would have monthly archives for the documentation, so that we could link to the version of number_field from October 2021 and it will still work in October 2027 when we're done with the mathlib5 port.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
| Alternatively, we can parse ((algebraic number) theory) as the area of mathematics studying [algebraic](https://leanprover-community.github.io/mathlib_docs/ring_theory/algebraic.html#is_algebraic) numbers, those satisfying a polynomial equation $f(\alpha) = 0$ for some nonzero polynomial $f$ with rational coefficients. | ||
| Algebraic numbers are found in [*number fields*](https://leanprover-community.github.io/mathlib_docs/number_theory/number_field.html#number_field), which are finite extensions of the field of rational numbers, | ||
| or equivalently fields generated by adjoining an algebraic element $\alpha$ to $\Q$ (by virtue of the [primitive element theorem](https://leanprover-community.github.io/mathlib_docs/field_theory/primitive_element.html#field.exists_primitive_element)). | ||
| Much like $\Q$ contains the integers $\Z$ as a subring, a number field $K$ contains a [*ring of integers*](https://leanprover-community.github.io/mathlib_docs/number_theory/number_field.html#number_field.ring_of_integers) $O_K$, |
There was a problem hiding this comment.
I agree with Eric's point, however I do think it's really cool that, like Wikipedia or nlab, we can talk about concepts and then directly link to them, so I absolutely think we should have some sort of link here.
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
|
I went through and updated the blog post. The main change is a new paragraph on the timeout issues I ended up solving by defining |
simply adding a parenthesis asserting words will be explained
|
Thanks a lot Anne! |
As requested, I wrote a bit on number theory, more specifically the Dedekind domain and class number formalization. The text is basically a summary of the class number paper, giving some mathematical background and pointing to the formal equivalents. I'm happy to have this blog post be edited mercilessly.
Is there a way to add commands like
\Z = \mathbb{Z}in the math blocks?Closes: #5