Skip to content

Commit

Permalink
chore(topology/instances/real): remove instance real_maps_algebra (#…
Browse files Browse the repository at this point in the history
…6920)

Remove 
```lean
instance reals_semimodule : has_continuous_smul ℝ ℝ
instance real_maps_algebra {α : Type*} [topological_space α] : algebra ℝ C(α, ℝ)
```
These are not used explicitly anywhere in the library, I suspect because if needed they can be found by typeclass inference.  Deleting them cleans up the import hierarchy by requiring many fewer files to import `topology.continuous_function.algebra`.
  • Loading branch information
hrmacbeth committed Mar 29, 2021
1 parent cb1d1c6 commit 5ab177a
Show file tree
Hide file tree
Showing 3 changed files with 2 additions and 6 deletions.
1 change: 1 addition & 0 deletions src/measure_theory/ae_eq_fun.lean
Expand Up @@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Zhouhang Zhou
-/
import measure_theory.integration
import order.filter.germ
import topology.continuous_function.algebra

/-!
Expand Down
1 change: 1 addition & 0 deletions src/topology/continuous_function/bounded.lean
Expand Up @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel, Mario Carneiro, Yury Kudryashov, Heather Macbeth
-/
import analysis.normed_space.basic
import topology.continuous_function.algebra

/-!
# Bounded continuous functions
Expand Down
6 changes: 0 additions & 6 deletions src/topology/instances/real.lean
Expand Up @@ -6,7 +6,6 @@ Authors: Johannes Hölzl, Mario Carneiro
import topology.metric_space.basic
import topology.algebra.uniform_group
import topology.algebra.ring
import topology.continuous_function.algebra
import ring_theory.subring
import group_theory.archimedean
/-!
Expand Down Expand Up @@ -285,11 +284,6 @@ eq_Icc_of_connected_compact ⟨(nonempty_Icc.2 hab).image f, is_preconnected_Icc

end

instance reals_semimodule : has_continuous_smul ℝ ℝ := ⟨continuous_mul⟩

instance real_maps_algebra {α : Type*} [topological_space α] :
algebra ℝ C(α, ℝ) := continuous_map_algebra

section subgroups

/-- Given a nontrivial subgroup `G ⊆ ℝ`, if `G ∩ ℝ_{>0}` has no minimum then `G` is dense. -/
Expand Down

0 comments on commit 5ab177a

Please sign in to comment.