chore(algebra/algebra/basic): show that the ℚ-algebra structure is un…

…ique (#5980)

Note that we already have similar lemmas showing that ℕ and ℤ modules are unique.

The name is based on `rat.algebra_rat`, which provides a canonical instance.

src/algebra/algebra/basic.lean

@@ -1016,6 +1016,11 @@ instance algebra_rat {α} [division_ring α] [char_zero α] : algebra ℚ α :=
 @[simp] theorem algebra_map_rat_rat : algebra_map ℚ ℚ = ring_hom.id ℚ :=
 subsingleton.elim _ _
 
+-- TODO[gh-6025]: make this an instance once safe to do so
+lemma algebra_rat_subsingleton {α} [semiring α] :
+  subsingleton (algebra ℚ α) :=
+⟨λ x y, algebra.algebra_ext x y $ ring_hom.congr_fun $ subsingleton.elim _ _⟩
+
 end rat
 
 namespace algebra