feat: port Data.Multiset.NatAntidiagonal (#1561)

Mathlib.lean

@@ -294,6 +294,7 @@ import Mathlib.Data.Multiset.Bind
 import Mathlib.Data.Multiset.Dedup
 import Mathlib.Data.Multiset.FinsetOps
 import Mathlib.Data.Multiset.Fold
+import Mathlib.Data.Multiset.NatAntidiagonal
 import Mathlib.Data.Multiset.Nodup
 import Mathlib.Data.Multiset.Pi
 import Mathlib.Data.Multiset.Powerset

Mathlib/Data/Multiset/NatAntidiagonal.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2019 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+
+! This file was ported from Lean 3 source module data.multiset.nat_antidiagonal
+! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.Multiset.Nodup
+import Mathlib.Data.List.NatAntidiagonal
+
+/-!
+# Antidiagonals in ℕ × ℕ as multisets
+
+This file defines the antidiagonals of ℕ × ℕ as multisets: the `n`-th antidiagonal is the multiset
+of pairs `(i, j)` such that `i + j = n`. This is useful for polynomial multiplication and more
+generally for sums going from `0` to `n`.
+
+## Notes
+
+This refines file `Data.List.NatAntidiagonal` and is further refined by file
+`Data.Finset.NatAntidiagonal`.
+-/
+
+namespace Multiset
+
+namespace Nat
+
+/-- The antidiagonal of a natural number `n` is
+    the multiset of pairs `(i, j)` such that `i + j = n`. -/
+def antidiagonal (n : ℕ) : Multiset (ℕ × ℕ) :=
+  List.Nat.antidiagonal n
+#align multiset.nat.antidiagonal Multiset.Nat.antidiagonal
+
+/-- A pair (i, j) is contained in the antidiagonal of `n` if and only if `i + j = n`. -/
+@[simp]
+theorem mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} : x ∈ antidiagonal n ↔ x.1 + x.2 = n := by
+  rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]
+#align multiset.nat.mem_antidiagonal Multiset.Nat.mem_antidiagonal
+
+/-- The cardinality of the antidiagonal of `n` is `n+1`. -/
+@[simp]
+theorem card_antidiagonal (n : ℕ) : card (antidiagonal n) = n + 1 := by
+  rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]
+#align multiset.nat.card_antidiagonal Multiset.Nat.card_antidiagonal
+
+/-- The antidiagonal of `0` is the list `[(0, 0)]` -/
+@[simp]
+theorem antidiagonal_zero : antidiagonal 0 = {(0, 0)} :=
+  rfl
+#align multiset.nat.antidiagonal_zero Multiset.Nat.antidiagonal_zero
+
+/-- The antidiagonal of `n` does not contain duplicate entries. -/
+@[simp]
+theorem nodup_antidiagonal (n : ℕ) : Nodup (antidiagonal n) :=
+  coe_nodup.2 <| List.Nat.nodup_antidiagonal n
+#align multiset.nat.nodup_antidiagonal Multiset.Nat.nodup_antidiagonal
+
+@[simp]
+theorem antidiagonal_succ {n : ℕ} :
+    antidiagonal (n + 1) = (0, n + 1) ::ₘ (antidiagonal n).map (Prod.map Nat.succ id) := by
+  simp only [antidiagonal, List.Nat.antidiagonal_succ, coe_map, cons_coe]
+#align multiset.nat.antidiagonal_succ Multiset.Nat.antidiagonal_succ
+
+theorem antidiagonal_succ' {n : ℕ} :
+    antidiagonal (n + 1) = (n + 1, 0) ::ₘ (antidiagonal n).map (Prod.map id Nat.succ) := by
+  rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, add_comm, antidiagonal, coe_map,
+    coe_add, List.singleton_append, cons_coe]
+#align multiset.nat.antidiagonal_succ' Multiset.Nat.antidiagonal_succ'
+
+theorem antidiagonal_succ_succ' {n : ℕ} :
+    antidiagonal (n + 2) =
+      (0, n + 2) ::ₘ (n + 2, 0) ::ₘ (antidiagonal n).map (Prod.map Nat.succ Nat.succ) :=
+  by
+  rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod_map]
+  rfl
+#align multiset.nat.antidiagonal_succ_succ' Multiset.Nat.antidiagonal_succ_succ'
+
+theorem map_swap_antidiagonal {n : ℕ} : (antidiagonal n).map Prod.swap = antidiagonal n := by
+  rw [antidiagonal, coe_map, List.Nat.map_swap_antidiagonal, coe_reverse]
+#align multiset.nat.map_swap_antidiagonal Multiset.Nat.map_swap_antidiagonal
+
+end Nat
+
+end Multiset