Mathlib v3 is deprecated. Go to Mathlib v4

Theorem rat.algebra_rat_subsingleton

Modification history

2021-12-18 06:26
src/algebra/algebra/basic.lean
chore(algebra/algebra/basic): fix instances names to make doc links work (#10834) …
Deleted rat.algebra_rat_subsingletonView on Github →
2021-02-05 12:11
src/algebra/algebra/basic.lean
chore(algebra/algebra/basic): show that the ℚ-algebra structure is unique (#5980) …
Added rat.algebra_rat_subsingletonView on Github →