English
The set SMulAntidiagonal hs ht a consists of all pairs (g,p) with g ∈ s, p ∈ t and g • p = a.
Русский
Множество SMulAntidiagonal hs ht a состоит из всех пар (g,p) such, что g ∈ s, p ∈ t и g • p = a.
LaTeX
$$SMulAntidiagonal hs ht a ⊆ G × P with characteristic condition.$$
Lean4
/-- `Finset.SMulAntidiagonal hs ht a` is the set of all pairs of an element in `s` and an
element in `t` whose scalar multiplication yields `a`, but its construction requires proofs that `s`
and `t` are well-ordered. -/
@[to_additive /-- `Finset.VAddAntidiagonal hs ht a` is the set of all pairs of an element in `s`
and an element in `t` whose vector addition yields `a`, but its construction requires proofs that
`s` and `t` are well-ordered. -/
]
noncomputable def SMulAntidiagonal [PartialOrder G] [PartialOrder P] [IsOrderedCancelSMul G P] {s : Set G} {t : Set P}
(hs : s.IsPWO) (ht : t.IsPWO) (a : P) : Finset (G × P) :=
(SMulAntidiagonal.finite_of_isPWO hs ht a).toFinset
