Commit 2021-02-04 21:33 7734d386
View on Github →refactor(data/real/basic): make ℝ a structure (#6024) Preparation for :four_leaf_clover:, which doesn't have irreducible.
refactor(data/real/basic): make ℝ a structure (#6024) Preparation for :four_leaf_clover:, which doesn't have irreducible.