mathlib3

392ebecd - chore(algebra/algebra/basic): show that the ℚ-algebra structure is unique (#5980)

chore(algebra/algebra/basic): show that the ℚ-algebra structure is unique (#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.