Commit 2026-06-25 19:06 5c985547

feat(Algebra/Order/Antidiag/Prod): add HasMulAntidiagonal (#38623) We add a multiplicative version of Finset.HasAntidiagonal, called Finset.HasMulAntidiagonal. This requires some naming changes (since otherwise, for instance, there would be a clash between Finset.swap_mem_mulAntidiagonal and the corresponding lemma in Mathlib.Algebra.Order.Antidiag.Prod). We made the following naming choices:

• Since the additive version will be much more commonly used, we still keep Finset.HasAntidiagonal for the additive version, and translate mulAntidiagonal to antidiagonal rather than to addAntidiagonal. Note that in particular this affects the API in Mathlib.Data.Finset.MulAntidiagonal, which used addAntidiagonal.
• We move most of the results in Mathlib.Algebra.Order.Antidiag.Prod into the Has(Mul)Antidiagonal namespace, so that e.g. Finset.swap_mem_antidiagonal and Finset.HasAntidiagonal.mem_antidiagonal can co-exist. Note that some deprecation tags (e.g., for Finset.antidiagonal, Finset.antidiagonal.fst_le, ...) are intentionally missing. The reason is that antidiagonal and related lemmas are normally used inside an open Finset namespace, and since these declarations have moved into Finset.HasAntidiagonal, the deprecation causes errors which would require to explicitly add HasAntidiagonal in many places. An easier solution is just to open Finset.HasAntidiagonal, after which the preexisting code works. Co-authored-by : @xgenereux