Antidiagonal with values in general types #
We define a type class Finset.HasAntidiagonal A which contains a function
antidiagonal : A → Finset (A × A) such that antidiagonal n
is the finset of all pairs adding to n, as witnessed by mem_antidiagonal.
Analogously, the type class Finset.HasMulAntidiagonal A contains a function
mulAntidiagonal : A → Finset (A × A) such that mulAntidiagonal n
is the finset of all pairs multiplying to n, as witnessed by mem_mulAntidiagonal.
When A is a canonically ordered additive monoid with locally finite order
this typeclass can be instantiated with Finset.antidiagonalOfLocallyFinite.
This applies in particular when A is ℕ, more generally or σ →₀ ℕ,
or even ι →₀ A under the additional assumption OrderedSub A
that make it a canonically ordered additive monoid.
(In fact, we would just need an AddMonoid with a compatible order,
finite Iic, such that if a + b = n, then a, b ≤ n,
and any finiteness condition would be OK.)
For computational reasons it is better to manually provide instances for ℕ
and σ →₀ ℕ, to avoid quadratic runtime performance.
These instances are provided as Finset.Nat.instHasAntidiagonal and
Finsupp.instHasAntidiagonal.
This is why Finset.mulAntidiagonalOfLocallyFinite is an abbrev and not an instance.
This definition does not exactly match with that of Multiset.antidiagonal
defined in Mathlib/Data/Multiset/Antidiagonal.lean, because of the multiplicities.
Indeed, by counting multiplicities, Multiset α is equivalent to α →₀ ℕ,
but Finset.antidiagonal and Multiset.antidiagonal will return different objects.
For example, for s : Multiset ℕ := {0,0,0}, Multiset.antidiagonal s has 8 elements
but Finset.antidiagonal s has only 4.
def s : Multiset ℕ := {0, 0, 0}
#eval (Finset.antidiagonal s).card -- 4
#eval Multiset.card (Multiset.antidiagonal s) -- 8
TODO #
- For
PNat,HasMulAntidiagonalwill recover the set of divisors of a strictly positive integer.
The class of additive monoids with an antidiagonal.
The antidiagonal of an element
nis the finset of pairs(i, j)such thati + j = n.A pair belongs to
antidiagonal niff the sum of its components is equal ton.
Instances
The class of (multiplicative) monoids with a mulAntidiagonal.
The mulAntidiagonal of an element
nis the finset of pairs(i, j)such thati * j = n.A pair belongs to
mulAntidiagonal niff the product of its components is equal ton.
Instances
All HasMulAntidiagonal instances are equal
All HasAntidiagonal instances are equal
See also Finset.map_prodComm_mulAntidiagonal.
A point in the mulAntidiagonal is determined by its first coordinate.
See also Finset.mulAntidiagonal_congr'.
A point in the antidiagonal is determined by its first coordinate.
See also Finset.antidiagonal_congr'.
A point in the mulAntidiagonal is determined by its first co-ordinate (subtype version of
Finset.mulAntidiagonal_congr). This lemma is used by the ext tactic.
A point in the antidiagonal is determined by its first co-ordinate (subtype version of
Finset.antidiagonal_congr). This lemma is used by the ext tactic.
A point in the mulAntidiagonal is determined by its second coordinate.
See also Finset.mulAntidiagonal_congr.
A point in the antidiagonal is determined by its second coordinate.
See also Finset.antidiagonal_congr.
The disjoint union of mulAntidiagonals Σ (n : A), mulAntidiagonal n is equivalent to the
product A × A. This is such an equivalence, obtained by mapping (n, (k, l)) to (k, l).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The disjoint union of antidiagonals Σ (n : A), antidiagonal n is equivalent to the
product A × A. This is such an equivalence, obtained by mapping (n, (k, l)) to (k, l).
Equations
- One or more equations did not get rendered due to their size.
Instances For
In a canonically ordered multiplicative monoid, the mulAntidiagonal can be constructed by filtering.
Note that this is not an instance, as for sometimes a more efficient algorithm is available.
Equations
- Finset.HasMulAntidiagonal.mulAntidiagonalOfLocallyFinite = { mulAntidiagonal := fun (n : A) => {uv ∈ Finset.Iic n ×ˢ Finset.Iic n | uv.1 * uv.2 = n}, mem_mulAntidiagonal := ⋯ }
Instances For
In a canonically ordered additive monoid, the antidiagonal can be construct by filtering.
Note that this is not an instance, as for some times a more efficient algorithm is available.
Equations
- Finset.HasAntidiagonal.antidiagonalOfLocallyFinite = { antidiagonal := fun (n : A) => {uv ∈ Finset.Iic n ×ˢ Finset.Iic n | uv.1 + uv.2 = n}, mem_antidiagonal := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.