doc(*): blurbs galore

Document all `def`, `class`, and `inductive` that are reasonably public-facing

Author: digama0

algebra/big_operators.lean

@@ -14,6 +14,7 @@ variables {α : Type u} {β : Type v} {γ : Type w}
 namespace finset
 variables {s s₁ s₂ : finset α} {a : α} {f g : α → β}
 
+/-- `prod s f` is the product of `f x` as `x` ranges over the elements of the finite set `s`. -/
 @[to_additive finset.sum]
 protected def prod [comm_monoid β] (s : finset α) (f : α → β) : β := (s.1.map f).prod
 attribute [to_additive finset.sum.equations._eqn_1] finset.prod.equations._eqn_1

algebra/group.lean

@@ -325,6 +325,7 @@ end ordered_comm_group
 
 variables {β : Type*} [group α] [group β] {a b : α}
 
+/-- Predicate for group homomorphism. -/
 def is_group_hom (f : α → β) : Prop :=
 ∀ a b : α, f (a * b) = f a * f b
 
@@ -342,6 +343,8 @@ inv_eq_of_mul_eq_one $ by simp [(H a a⁻¹).symm, one H]
 
 end is_group_hom
 
+/-- Predicate for group anti-homomorphism, or a homomorphism
+  into the opposite group. -/
 def is_group_anti_hom (f : α → β) : Prop :=
 ∀ a b : α, f (a * b) = f b * f a
 

algebra/group_power.lean

@@ -21,6 +21,7 @@ variable {α : Type u}
 @[simp] theorem inv_inv' [discrete_field α] {a:α} : a⁻¹⁻¹ = a :=
 by rw [inv_eq_one_div, inv_eq_one_div, div_div_eq_mul_div]; simp [div_one]
 
+/-- The power operation in a monoid. `a^n = a*a*...*a` n times. -/
 def monoid.pow [monoid α] (a : α) : ℕ → α
 | 0     := 1
 | (n+1) := a * monoid.pow n
@@ -143,6 +144,10 @@ end nat
 
 open int
 
+/--
+The power operation in a group. This extends `monoid.pow` to negative integers
+with the definition `a^(-n) = (a^n)⁻¹`.
+-/
 @[simp] def gpow (a : α) : ℤ → α
 | (of_nat n) := a^n
 | -[1+n]     := (a^(nat.succ n))⁻¹

algebra/linear_algebra/basic.lean

@@ -62,6 +62,8 @@ finset.smul_sum
 
 end finsupp
 
+/-- The type of linear coefficients, which are simply the finitely supported functions
+from the module `β` to the scalar ring `α`. -/
 @[reducible] def lc (α : Type u) (β : Type v) [ring α] [module α β] : Type (max u v) := β →₀ α
 
 namespace lc
@@ -120,6 +122,7 @@ variables [ring α] [module α β] [module α γ] [module α δ]
 variables {a a' : α} {s t : set β} {b b' b₁ b₂ : β}
 include α
 
+/-- Linear span of a set of vectors -/
 def span (s : set β) : set β := { x | ∃(v : lc α β), (∀x∉s, v x = 0) ∧ x = v.sum (λb a, a • b) }
 
 @[instance] lemma is_submodule_span : is_submodule (span s) :=
@@ -213,6 +216,7 @@ lemma linear_eq_on {f g : β → γ} (hf : is_linear_map f) (hg : is_linear_map
     simp [this, h, hf.smul, hg.smul]
   end
 
+/-- Linearly independent set of vectors -/
 def linear_independent (s : set β) : Prop :=
 ∀l : lc α β, (∀x∉s, l x = 0) → l.sum (λv c, c • v) = 0 → l = 0
 
@@ -432,6 +436,7 @@ lemma linear_independent.eq_0_of_span : ∀a∈span s, f a = 0 → a = 0
 
 end
 
+/-- A set of vectors is a basis if it is linearly independent and all vectors are in the span -/
 def is_basis (s : set β) := linear_independent s ∧ (∀x, x ∈ span s)
 
 section is_basis

algebra/linear_algebra/linear_map_module.lean

@@ -23,6 +23,7 @@ hpq _ $ some_spec _
 
 end classical
 
+/-- The type of linear maps `β → γ` between α-modules β and γ -/
 def linear_map {α : Type u} (β : Type v) (γ : Type w) [ring α] [module α β] [module α γ] :=
 subtype (@is_linear_map α β γ _ _ _)
 
@@ -45,6 +46,7 @@ lemma is_linear_map_coe : is_linear_map A := A.property
 
 /- kernel -/
 
+/-- Kernel of a linear map, i.e. the set of vectors mapped to zero by the map -/
 def ker (A : linear_map β γ) : set β := {y | A y = 0}
 
 section ker
@@ -71,6 +73,7 @@ end ker
 
 /- image -/
 
+/-- Image of a linear map, the set of vectors of the form `A x` for some β -/
 def im (A : linear_map β γ) : set γ := {x | ∃ y, A y = x}
 
 @[simp] lemma mem_im {A : linear_map β γ} {z : γ} :
@@ -222,6 +225,7 @@ def endomorphism_ring : ring (linear_map β β) :=
 by refine {mul := (*), one := 1, ..linear_map.add_comm_group, ..};
   { intros, apply linear_map.ext, simp }
 
+/-- The group of invertible linear maps from `β` to itself -/
 def general_linear_group :=
 @units (linear_map β β) (@ring.to_semiring _ (endomorphism_ring α β))
 

algebra/linear_algebra/multivariate_polynomial.lean

@@ -20,6 +20,7 @@ instance {α : Type u} [semilattice_sup α] : is_idempotent α (⊔) := ⟨assum
 namespace finset
 variables [semilattice_sup_bot α]
 
+/-- Supremum of a finite set: `sup {a, b, c} f = f a ⊔ f b ⊔ f c` -/
 def sup (s : finset β) (f : β → α) : α := s.fold (⊔) ⊥ f
 
 variables {s s₁ s₂ : finset β} {f : β → α}
@@ -91,6 +92,8 @@ have ∀(s : finset α) (f : α →₀ β), s = f.support → p f,
       end),
 this _ _ rfl
 
+/-- Multivariate polynomial, where `σ` is the index set of the variables and
+  `α` is the coefficient ring -/
 def mv_polynomial (σ : Type*) (α : Type*) [comm_semiring α] := (σ →₀ ℕ) →₀ α
 
 namespace mv_polynomial
@@ -105,10 +108,13 @@ instance : has_add (mv_polynomial σ α) := finsupp.has_add
 instance : has_mul (mv_polynomial σ α) := finsupp.has_mul
 instance : comm_semiring (mv_polynomial σ α) := finsupp.to_comm_semiring
 
+/-- monomial s a is the monomial `a * X^s` -/
 def monomial (s : σ →₀ ℕ) (a : α) : mv_polynomial σ α := single s a
 
+/-- C a is the constant polynomial with value a -/
 def C (a : α) : mv_polynomial σ α := monomial 0 a
 
+/-- X n is the polynomial with value X_n -/
 def X (n : σ) : mv_polynomial σ α := monomial (single n 1) 1
 
 @[simp] lemma C_0 : C 0 = (0 : mv_polynomial σ α) := by simp [C, monomial]; refl
@@ -165,6 +171,7 @@ finsupp.single_induction_on p
 section eval
 variables {f : σ → α}
 
+/-- Evaluate a polynomial `p` given a valuation `f` of all the variables -/
 def eval (p : mv_polynomial σ α) (f : σ → α) : α :=
 p.sum (λs a, a * s.prod (λn e, f n ^ e))
 
@@ -209,6 +216,7 @@ end eval
 
 section vars
 
+/-- `vars p` is the set of variables appearing in the polynomial `p` -/
 def vars (p : mv_polynomial σ α) : finset σ := p.support.bind finsupp.support
 
 @[simp] lemma vars_0 : (0 : mv_polynomial σ α).vars = ∅ :=
@@ -230,11 +238,13 @@ calc (X n : mv_polynomial σ α).vars = (single n 1).support : vars_monomial h.s
 end vars
 
 section degree_of
+/-- `degree_of n p` gives the highest power of X_n that appears in `p` -/
 def degree_of (n : σ) (p : mv_polynomial σ α) : ℕ := p.support.sup (λs, s n)
 
 end degree_of
 
 section total_degree
+/-- `total_degree p` gives the maximum |s| over the monomials X^s in `p` -/
 def total_degree (p : mv_polynomial σ α) : ℕ := p.support.sup (λs, s.sum $ λn e, e)
 
 end total_degree

algebra/linear_algebra/quotient_module.lean

@@ -33,6 +33,7 @@ lemma quotient_rel_eq {b₁ b₂ : β} : (b₁ ≈ b₂) = (b₁ - b₂ ∈ s) :
 
 section
 variable (β)
+/-- Quotient module. `quotient β s` is the quotient of the module `β` by the submodule `s`. -/
 def quotient : Type v := quotient (quotient_rel s)
 end
 

algebra/module.lean

@@ -15,10 +15,16 @@ variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 lemma set.sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂i ∈ s, i) :=
 set.ext $ by simp
 
+/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
 class has_scalar (α : out_param $ Type u) (γ : Type v) := (smul : α → γ → γ)
 
 infixr ` • `:73 := has_scalar.smul
 
+/-- A module is a generalization of vector spaces to a scalar ring.
+  It consists of a scalar ring `α` and an additive group of "vectors" `β`,
+  connected by a "scalar multiplication" operation `r • x : β`
+  (where `r : α` and `x : β`) with some natural associativity and
+  distributivity axioms similar to those on a ring. -/
 class module (α : out_param $ Type u) (β : Type v) [out_param $ ring α]
   extends has_scalar α β, add_comm_group β :=
 (smul_add : ∀r (x y : β), r • (x + y) = r • x + r • y)
@@ -143,6 +149,9 @@ by refine {..}; simp [hf.add, hf.smul, add_smul, smul_smul]
 
 end is_linear_map
 
+/-- A submodule of a module is one which is closed under vector operations.
+  This is a sufficient condition for the subset of vectors in the submodule
+  to themselves form a module. -/
 class is_submodule {α : Type u} {β : Type v} [ring α] [module α β] (p : set β) : Prop :=
 (zero_ : (0:β) ∈ p)
 (add_  : ∀ {x y}, x ∈ p → y ∈ p → x + y ∈ p)
@@ -221,8 +230,14 @@ end
 
 end is_submodule
 
+/-- A vector space is the same as a module, except the scalar ring is actually
+  a field. (This adds commutativity of the multiplication and existence of inverses.)
+  This is the traditional generalization of spaces like `ℝ^n`, which have a natural
+  addition operation and a way to multiply them by real numbers, but no multiplication
+  operation between vectors. -/
 class vector_space (α : out_param $ Type u) (β : Type v) [field α] extends module α β
 
+/-- Subspace of a vector space. Defined to equal `is_submodule`. -/
 @[reducible] def subspace {α : Type u} {β : Type v} [field α] [vector_space α β] (p : set β) :
   Prop :=
 is_submodule p

algebra/order.lean

@@ -75,6 +75,8 @@ le_antisymm ((H _).2 (le_refl _)) ((H _).1 (le_refl _))
 
 namespace ordering
 
+/-- `compares o a b` means that `a` and `b` have the ordering relation
+  `o` between them, assuming that the relation `a < b` is defined -/
 @[simp] def compares [has_lt α] : ordering → α → α → Prop
 | lt a b := a < b
 | eq a b := a = b

algebra/ordered_group.lean

@@ -14,10 +14,18 @@ section old_structure_cmd
 
 set_option old_structure_cmd true
 
+/-- An ordered (additive) commutative monoid is a commutative monoid 
+  with a partial order such that addition is an order embedding, i.e.
+  `a + b ≤ a + c ↔ b ≤ c`. These monoids are automatically cancellative. -/
 class ordered_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=
 (add_le_add_left       : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
 (lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)
 
+/-- A canonically ordered monoid is an ordered commutative monoid
+  in which the ordering coincides with the divisibility relation,
+  which is to say, `a ≤ b` iff there exists `c` with `b = a + c`.
+  This is satisfied by the natural numbers, for example, but not
+  the integers or other ordered groups. -/
 class canonically_ordered_monoid (α : Type*) extends ordered_comm_monoid α :=
 (le_iff_exists_add : ∀a b:α, a ≤ b ↔ ∃c, b = a + c)
 
@@ -335,9 +343,9 @@ sub_left_lt_iff_lt_add.trans (lt_add_iff_pos_left _)
 
 end ordered_comm_group
 
--- This is not so much a new structure as a construction mechanism
--- for ordered groups
 set_option old_structure_cmd true
+/-- This is not so much a new structure as a construction mechanism
+  for ordered groups, by specifying only the "positive cone" of the group. -/
 class nonneg_comm_group (α : Type*) extends add_comm_group α :=
 (nonneg : α → Prop)
 (pos : α → Prop := λ a, nonneg a ∧ ¬ nonneg (neg a))