English
For a given subsets s,t and element a, mulAntidiagonal hs ht a is the finite set of all pairs (x,y) with x ∈ s, y ∈ t, and x·y = a.
Русский
Для данных множеств s,t и элемента a, mulAntidiagonal hs ht a есть конечное множество пар (x,y) таких что x ∈ s, y ∈ t и x·y = a.
LaTeX
$$mulAntidiagonal hs ht a = { (x,y) ∈ s × t | x y = a }$$
Lean4
/-- `Finset.mulAntidiagonal hs ht a` is the set of all pairs of an element in `s` and an
element in `t` that multiply to `a`, but its construction requires proofs that `s` and `t` are
well-ordered. -/
@[to_additive /-- `Finset.addAntidiagonal hs ht a` is the set of all pairs of an element in
`s` and an element in `t` that add to `a`, but its construction requires proofs that `s` and `t` are
well-ordered. -/
]
noncomputable def mulAntidiagonal : Finset (α × α) :=
(Set.MulAntidiagonal.finite_of_isPWO hs ht a).toFinset
