Commit 2022-12-04 12:17 1a766f5a
View on Github →feat(data/real/basic): remove typeclass shortcircuit (#17804)
The only remaining use of module in data/real/basic and its prerequisites is to provide the typeclass shortcircuit
instance : module ℝ ℝ := by apply_instance
I propose deleting this.