chore(algebra/algebra/basic): fix instances names to make doc links work (#10834)

The blank lines avoid sentences being pulled into the bulleted list above them.

Author: eric-wieser

src/algebra/algebra/basic.lean

@@ -37,7 +37,7 @@ See the implementation notes for remarks about non-associative and non-unital al
   * `algebra_nat`
   * `algebra_int`
   * `algebra_rat`
-  * `opposite.algebra`
+  * `mul_opposite.algebra`
   * `module.End.algebra`
 
 ## Notations
@@ -67,6 +67,7 @@ As a result, there are two ways to talk about an `R`-algebra `A` when `A` is a s
    variables [comm_semiring R] [semiring A]
    variables [module R A] [smul_comm_class R A A] [is_scalar_tower R A A]
    ```
+
 The first approach implies the second via typeclass search; so any lemma stated with the second set
 of arguments will automatically apply to the first set. Typeclass search does not know that the
 second approach implies the first, but this can be shown with:
@@ -87,6 +88,7 @@ all be relaxed independently; for instance, this allows us to:
 * Replace `comm_semiring R` and `module R A` with `comm_group R'` and `distrib_mul_action R' A`,
   which when `R' = units R` lets us talk about the "algebra-like" action of `units R` on an
   `R`-algebra `A`.
+
 While `alg_hom R A B` cannot be used in the second approach, `non_unital_alg_hom R A B` still can.
 
 You should always use the first approach when working with associative unital algebras, and mimic
@@ -311,7 +313,7 @@ end id
 section prod
 variables (R A B)
 
-instance : algebra R (A × B) :=
+instance _root_.prod.algebra : algebra R (A × B) :=
 { commutes' := by { rintro r ⟨a, b⟩, dsimp, rw [commutes r a, commutes r b] },
   smul_def' := by { rintro r ⟨a, b⟩, dsimp, rw [smul_def r a, smul_def r b] },
   .. prod.module,
@@ -1258,7 +1260,7 @@ def to_rat_alg_hom [ring R] [ring S] [algebra ℚ R] [algebra ℚ S] (f : R →+
 
 end ring_hom
 
-namespace rat
+section rat
 
 instance algebra_rat {α} [division_ring α] [char_zero α] : algebra ℚ α :=
 (rat.cast_hom α).to_algebra' $ λ r x, r.cast_commute x

src/number_theory/bernoulli.lean

@@ -282,7 +282,7 @@ begin
     apply sum_congr rfl,
     simp_intros m h only [finset.mem_range],
     simp only [f, exp_pow_eq_rescale_exp, rescale, one_div, coeff_mk, ring_hom.coe_mk, coeff_exp,
-              ring_hom.id_apply, cast_mul, rat.algebra_map_rat_rat],
+              ring_hom.id_apply, cast_mul, algebra_map_rat_rat],
     -- manipulate factorials and binomial coefficients
     rw [choose_eq_factorial_div_factorial h.le, eq_comm, div_eq_iff (hne q.succ), succ_eq_add_one,
         mul_assoc _ _ ↑q.succ!, mul_comm _ ↑q.succ!, ← mul_assoc, div_mul_eq_mul_div,