Create has_antidiagonal class
#7917
Comments
bors bot
pushed a commit
that referenced
this issue
Oct 31, 2023
…7486) 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`. When `A` is a canonically ordered add 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 add 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.antidiagonalOfLocallyFinite` is an `abbrev` and not an `instance`. This definition does not exactly match with that of `Multiset.antidiagonal` defined in `Mathlib.Data.Multiset.Antidiagonal`, 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. ```lean def s : Multiset ℕ := {0, 0, 0} #eval (Finset.antidiagonal s).card -- 4 #eval Multiset.card (Multiset.antidiagonal s) -- 8 ``` ## TODO * Define `HasMulAntidiagonal` (for monoids). For `PNat`, we will recover the set of divisors of a strictly positive integer. This closes #7917 Co-authored by: María Inés de Frutos-Fernández <mariaines.dff@gmail.com> and Eric Wieser <efw27@cam.ac.uk> Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
grunweg
pushed a commit
that referenced
this issue
Nov 1, 2023
…7486) 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`. When `A` is a canonically ordered add 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 add 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.antidiagonalOfLocallyFinite` is an `abbrev` and not an `instance`. This definition does not exactly match with that of `Multiset.antidiagonal` defined in `Mathlib.Data.Multiset.Antidiagonal`, 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. ```lean def s : Multiset ℕ := {0, 0, 0} #eval (Finset.antidiagonal s).card -- 4 #eval Multiset.card (Multiset.antidiagonal s) -- 8 ``` ## TODO * Define `HasMulAntidiagonal` (for monoids). For `PNat`, we will recover the set of divisors of a strictly positive integer. This closes #7917 Co-authored by: María Inés de Frutos-Fernández <mariaines.dff@gmail.com> and Eric Wieser <efw27@cam.ac.uk> Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
fgdorais
pushed a commit
that referenced
this issue
Nov 1, 2023
…7486) 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`. When `A` is a canonically ordered add 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 add 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.antidiagonalOfLocallyFinite` is an `abbrev` and not an `instance`. This definition does not exactly match with that of `Multiset.antidiagonal` defined in `Mathlib.Data.Multiset.Antidiagonal`, 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. ```lean def s : Multiset ℕ := {0, 0, 0} #eval (Finset.antidiagonal s).card -- 4 #eval Multiset.card (Multiset.antidiagonal s) -- 8 ``` ## TODO * Define `HasMulAntidiagonal` (for monoids). For `PNat`, we will recover the set of divisors of a strictly positive integer. This closes #7917 Co-authored by: María Inés de Frutos-Fernández <mariaines.dff@gmail.com> and Eric Wieser <efw27@cam.ac.uk> Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Per @digama0 's suggestion here, we should create a class for antidiagonals on types.
The text was updated successfully, but these errors were encountered: