Loogle bug with export

Stream: general

[Kenny Lau]

Searching Finset.HasAntidiagonal.antidiagonal on Loogle will give you theorems mentioning Finset.antidiagonal, but searching Finset.antidiagonal gives you an "unknown identifier".

This is because antidiagonal has been exported out of the Finset.HasAntidiagonal namespace. @Joachim Breitner would you know how to fix this?

https://github.com/leanprover-community/mathlib4/blob/419963adcc5760a79f65f3368ec66c9555a41a18/Mathlib/Algebra/Order/Antidiag/Prod.lean#L54-L59

/-- The class of additive monoids with an antidiagonal -/
class HasAntidiagonal (A : Type*) [AddMonoid A] where
  /-- The antidiagonal of an element `n` is the finset of pairs `(i, j)` such that `i + j = n`. -/
  antidiagonal : A → Finset (A × A)
  /-- A pair belongs to `antidiagonal n` iff the sum of its components is equal to `n`. -/
  mem_antidiagonal {n} {a} : a ∈ antidiagonal n ↔ a.fst + a.snd = n

export HasAntidiagonal (antidiagonal mem_antidiagonal)

[Aaron Liu]

You can search @loogle (Finset.antidiagonal)

[loogle]

:search: Finset.hasAntidiagonal_congr, Finset.sigmaAntidiagonalEquivProd, and 109 more

[Aaron Liu]

if you put parentheses it interprets it as a term

[Joachim Breitner]

So loogle needs to use something else for name resolution? could someone report an issue at https://github.com/nomeata/loogle/issues/? Probably not hard to fix.