Commit 2024-06-11 07:52 fa87862b

chore: fix diamond for WithTop subtraction (#13715) We have currently two different subtractions on WithTop α.

• The first one, requiring that α has a zero, maps x - ⊤ to 0, and is the right convention when defining subtraction on ENat or ENNReal.
• The second one, requiring a LinearOrderedAddCommGroup, maps x - ⊤ to ⊤. It is the additivization of the usual convention x / 0 = 0, and is relevant to work with valuations. Both instances apply for example to WithTop ℤ, creating a diamond. This PR changes the first instance to require a bottom element instead of a zero, to make sure that the two instances will apply in disjoint situations. This requires some new API for the second instance, to fix Mathlib/Analysis/Analytic/Meromorphic.lean which was (incorrectly) using the first instance.