Commit 2025-03-17 08:40 2b2cc75b

feat: add WithTop.untop₀ (#22821) For types α that are instances of Zero, provide a convenient conversion, WithTop.toBase, that maps elements a : WithTop α to α, by mapping ⊤ to zero. For settings where α has additional structure, provide simplifier lemmas, akin to those already existing for ENat.toNat. This is PR implements a suggestion discussed on Zulip This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.