diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean
index f3ddc0a80c658..b05ce608fd563 100644
--- a/src/ring_theory/ideal/operations.lean
+++ b/src/ring_theory/ideal/operations.lean
@@ -22,9 +22,11 @@ variables [comm_ring R] [add_comm_group M] [module R M]
 instance has_scalar' : has_scalar (ideal R) (submodule R M) :=
 ⟨λ I N, ⨆ r : I, N.map (r.1 • linear_map.id)⟩
 
+/-- `N.annihilator` is the ideal of all elements `r : R` such that `r • N = 0`. -/
 def annihilator (N : submodule R M) : ideal R :=
 (linear_map.lsmul R N).ker
 
+/-- `N.colon P` is the ideal of all elements `r : R` such that `r • P ⊆ N`. -/
 def colon (N P : submodule R M) : ideal R :=
 annihilator (P.map N.mkq)
 
@@ -216,6 +218,8 @@ begin
   rw [ring_hom.map_mul, hφ1, mul_one]
 end
 
+/-- The homomorphism from `R/(⋂ i, f i)` to `∏ i, (R / f i)` featured in the Chinese
+  Remainder Theorem. It is bijective if the ideals `f i` are comaximal. -/
 def quotient_inf_to_pi_quotient (f : ι → ideal R) :
   (⨅ i, f i).quotient →+* Π i, (f i).quotient :=
 begin
@@ -458,6 +462,8 @@ variables {R : Type u} {S : Type v} [comm_ring R] [comm_ring S]
 variables (f : R →+* S)
 variables {I J : ideal R} {K L : ideal S}
 
+/-- `I.map f` is the span of the image of the ideal `I` under `f`, which may be bigger than
+  the image itself. -/
 def map (I : ideal R) : ideal S :=
 span (f '' I)
 
diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index 472f1fac4d0af..96b8033f8fe15 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -29,6 +29,7 @@ namespace multiplicity
 section comm_monoid
 variables [comm_monoid α]
 
+/-- `multiplicity.finite a b` indicates that the multiplicity of `a` in `b` is finite. -/
 @[reducible] def finite (a b : α) : Prop := ∃ n : ℕ, ¬a ^ (n + 1) ∣ b
 
 lemma finite_iff_dom [decidable_rel ((∣) : α → α → Prop)] {a b : α} :
diff --git a/src/ring_theory/ring_invo.lean b/src/ring_theory/ring_invo.lean
index 26155710be68b..2354d57d2202f 100644
--- a/src/ring_theory/ring_invo.lean
+++ b/src/ring_theory/ring_invo.lean
@@ -68,6 +68,7 @@ open ring_invo
 section comm_ring
 variables [comm_ring R]
 
+/-- The identity function of a `comm_ring` is a ring involution. -/
 protected def ring_invo.id : ring_invo R :=
 { involution' := λ r, rfl,
   ..(ring_equiv.to_opposite R) }