docs(data/*/nat_antidiagonal): add one module docstring and harmonise…

… others (#7919)

src/data/finset/nat_antidiagonal.lean

@@ -7,28 +7,35 @@ import data.finset.basic
 import data.multiset.nat_antidiagonal
 
 /-!
-# The "antidiagonal" {(0,n), (1,n-1), ..., (n,0)} as a finset.
+# Antidiagonals in ℕ × ℕ as finsets
+
+This file defines the antidiagonals of ℕ × ℕ as finsets: the `n`-th antidiagonal is the finset 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 files `data.list.nat_antidiagonal` and `data.multiset.nat_antidiagonal`.
 -/
 
 namespace finset
-
 namespace nat
 
 /-- The antidiagonal of a natural number `n` is
-    the finset of pairs `(i,j)` such that `i+j = n`. -/
+    the finset of pairs `(i, j)` such that `i + j = n`. -/
 def antidiagonal (n : ℕ) : finset (ℕ × ℕ) :=
 ⟨multiset.nat.antidiagonal n, multiset.nat.nodup_antidiagonal n⟩
 
-/-- A pair (i,j) is contained in the antidiagonal of `n` if and only if `i+j=n`. -/
+/-- A pair (i, j) is contained in the antidiagonal of `n` if and only if `i + j = n`. -/
 @[simp] lemma mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} :
   x ∈ antidiagonal n ↔ x.1 + x.2 = n :=
 by rw [antidiagonal, mem_def, multiset.nat.mem_antidiagonal]
 
-/-- The cardinality of the antidiagonal of `n` is `n+1`. -/
+/-- The cardinality of the antidiagonal of `n` is `n + 1`. -/
 @[simp] lemma card_antidiagonal (n : ℕ) : (antidiagonal n).card = n+1 :=
 by simp [antidiagonal]
 
-/-- The antidiagonal of `0` is the list `[(0,0)]` -/
+/-- The antidiagonal of `0` is the list `[(0, 0)]` -/
 @[simp] lemma antidiagonal_zero : antidiagonal 0 = {(0, 0)} :=
 rfl
 

src/data/list/nat_antidiagonal.lean

@@ -5,16 +5,29 @@ Authors: Johan Commelin
 -/
 import data.list.range
 
+/-!
+# Antidiagonals in ℕ × ℕ as lists
+
+This file defines the antidiagonals of ℕ × ℕ as lists: the `n`-th antidiagonal is the list 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
+
+Files `data.multiset.nat_antidiagonal` and `data.finset.nat_antidiagonal` successively turn the
+`list` definition we have here into `multiset` and `finset`.
+-/
+
 open list function nat
 
 namespace list
 namespace nat
 
-/-- The antidiagonal of a natural number `n` is the list of pairs `(i,j)` such that `i+j = n`. -/
+/-- The antidiagonal of a natural number `n` is the list of pairs `(i, j)` such that `i + j = n`. -/
 def antidiagonal (n : ℕ) : list (ℕ × ℕ) :=
 (range (n+1)).map (λ i, (i, n - i))
 
-/-- A pair (i,j) is contained in the antidiagonal of `n` if and only if `i+j=n`. -/
+/-- A pair (i, j) is contained in the antidiagonal of `n` if and only if `i + j = n`. -/
 @[simp] lemma mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} :
   x ∈ antidiagonal n ↔ x.1 + x.2 = n :=
 begin
@@ -25,11 +38,11 @@ begin
     { exact prod.ext rfl (nat.add_sub_cancel_left _ _) } }
 end
 
-/-- The length of the antidiagonal of `n` is `n+1`. -/
+/-- The length of the antidiagonal of `n` is `n + 1`. -/
 @[simp] lemma length_antidiagonal (n : ℕ) : (antidiagonal n).length = n+1 :=
 by rw [antidiagonal, length_map, length_range]
 
-/-- The antidiagonal of `0` is the list `[(0,0)]` -/
+/-- The antidiagonal of `0` is the list `[(0, 0)]` -/
 @[simp] lemma antidiagonal_zero : antidiagonal 0 = [(0, 0)] :=
 rfl
 
@@ -40,7 +53,7 @@ nodup_map (@left_inverse.injective ℕ (ℕ × ℕ) prod.fst (λ i, (i, n-i)) $
 @[simp] lemma antidiagonal_succ {n : ℕ} :
   antidiagonal (n + 1) = (0, n + 1) :: ((antidiagonal n).map (prod.map nat.succ id) ) :=
 begin
-  simp only [antidiagonal, range_succ_eq_map, map_cons, true_and, nat.add_succ_sub_one, add_zero, 
+  simp only [antidiagonal, range_succ_eq_map, map_cons, true_and, nat.add_succ_sub_one, add_zero,
     id.def, eq_self_iff_true, nat.sub_zero, map_map, prod.map_mk],
   apply congr (congr rfl _) rfl,
   ext; simp,

src/data/multiset/nat_antidiagonal.lean

@@ -7,18 +7,27 @@ import data.multiset.nodup
 import data.list.nat_antidiagonal
 
 /-!
-# The "antidiagonal" {(0,n), (1,n-1), ..., (n,0)} as a multiset.
+# 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.nat_antidiagonal` and is further refined by file
+`data.finset.nat_antidiagonal`.
 -/
 
 namespace multiset
 namespace nat
 
 /-- The antidiagonal of a natural number `n` is
-    the multiset of pairs `(i,j)` such that `i+j = n`. -/
+    the multiset of pairs `(i, j)` such that `i + j = n`. -/
 def antidiagonal (n : ℕ) : multiset (ℕ × ℕ) :=
 list.nat.antidiagonal n
 
-/-- A pair (i,j) is contained in the antidiagonal of `n` if and only if `i+j=n`. -/
+/-- A pair (i, j) is contained in the antidiagonal of `n` if and only if `i + j = n`. -/
 @[simp] lemma mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} :
   x ∈ antidiagonal n ↔ x.1 + x.2 = n :=
 by rw [antidiagonal, mem_coe, list.nat.mem_antidiagonal]
@@ -27,7 +36,7 @@ by rw [antidiagonal, mem_coe, list.nat.mem_antidiagonal]
 @[simp] lemma card_antidiagonal (n : ℕ) : (antidiagonal n).card = n+1 :=
 by rw [antidiagonal, coe_card, list.nat.length_antidiagonal]
 
-/-- The antidiagonal of `0` is the list `[(0,0)]` -/
+/-- The antidiagonal of `0` is the list `[(0, 0)]` -/
 @[simp] lemma antidiagonal_zero : antidiagonal 0 = {(0, 0)} :=
 rfl