maria.defrutos@uam.es
El objetivo de esta charla es presentar una formalización en el asistente interactivo de demostración Lean de la teoría básica de los cuerpos discretamente valorados. En particular, demostramos que la bola unidad con respecto a una valoración discreta en un cuerpo es un anillo de valoración discreta y, recíprocamente, que la valoración ádica en el cuerpo de fracciones de un anillo de valoración discreta es discreta. Definimos extensiones finitas de valoraciones y de anillos de valoración discreta, y probamos algunos resultados de tipo global a local. Partiendo de esta teoría general, formalizamos la definición abstracta y algunas propiedades fundamentales de los cuerpos locales, y demostramos que las extensiones finitas del cuerpo $\mathbb{Q}_p$ de números $p$-ádicos y el cuerpo $\mathbb{F}_p(!(X)!)$ de series de Laurent sobre $\mathbb{F}_p$ son cuerpos locales. Este proyecto es un trabajo conjunto con Filippo Nuccio.