lint(group_theory/*): docstrings and an inhabited instance (#4493)

An inhabited instance for `presented_group`
Docstrings in `group_theory/abelianization` and `group_theory/congruence`.



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/group_theory/abelianization.lean

@@ -63,6 +63,8 @@ begin
   simp [monoid_hom.mem_ker, mul_right_comm (f p) (f q)],
 end
 
+/-- If `f : G → A` is a group homomorphism to an abelian group, then `lift f` is the unique map from
+  the abelianization of a `G` to `A` that factors through `f`. -/
 def lift : abelianization G →* A :=
 quotient_group.lift _ f (λ x h, f.mem_ker.2 $ commutator_subset_ker _ h)
 

src/group_theory/congruence.lean

@@ -65,6 +65,12 @@ structure add_con [has_add M] extends setoid M :=
 @[to_additive add_con] structure con [has_mul M] extends setoid M :=
 (mul' : ∀ {w x y z}, r w x → r y z → r (w * y) (x * z))
 
+/-- The equivalence relation underlying an additive congruence relation. -/
+add_decl_doc add_con.to_setoid
+
+/-- The equivalence relation underlying a multiplicative congruence relation. -/
+add_decl_doc con.to_setoid
+
 variables {M}
 
 /-- The inductively defined smallest additive congruence relation containing a given binary

src/group_theory/presented_group.lean

@@ -58,4 +58,7 @@ theorem to_group.unique (g : presented_group rels →* β)
     (λ _, free_group.to_group.unique (g.comp (quotient_group.mk' _)) hg)
 
 end to_group
+
+instance (rels : set (free_group α)) : inhabited (presented_group rels) := ⟨1⟩
+
 end presented_group