Formalising the Bruhat-Tits tree

DOI10.46298/AFM.15738MaRDI QIDQ7319406zbMATH OpenFDO

Authors Judith Ludwig, Christian Merten

Publication date 25 August 2026

Published in Annals of Formalized Mathematics. AFM (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/AFM.15738

Mathematics Subject Classification ID

Groups acting on trees (20E08) Linear algebraic groups over local fields and their integers (20G25) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• Bruhat-Tits theory. A new approach
• Discrete groups, Mumford curves and theta functions
• Group cohomology in the Lean community library
• scientific article; zbMATH DE number 3813822 (Why is no real title available?)
• scientific article; zbMATH DE number 1842475 (Why is no real title available?)
• Non-Archimedean strings and Bruhat-Tits trees
• Reductive groups over a local field
• The p-adic upper half plane
• The Lean 4 theorem prover and programming language
• The Poisson Kernel for Drinfeld Modular Curves
• Values of p-adic L-functions and a p-adic Poisson kernel

This page was built for publication: Formalising the Bruhat-Tits tree

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7319406)