Theorems · Definition · combinatorics

Set.smulAntidiagonal

{G : Type u_1} → {P : Type u_2} → [SMul G P] → Set G → Set P → P → Set (G × P)

smulAntidiagonal s t a is the set of all pairs of an element in s and an element in t that scalar multiply to a.

Defined in

Mathlib.Data.Set.SMulAntidiagonal

Cited by

17 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

SMul