Commit 2021-02-05 12:11 392ebecd
View on Github →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.