Skip to content

Commit

Permalink
fix (topology/algebra/basic): fix universe issue with of_nhds_one (#6647
Browse files Browse the repository at this point in the history
)

Everything had type max{u v} before.
  • Loading branch information
kbuzzard committed Mar 11, 2021
1 parent 4d8d344 commit b1aafb2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/topology/algebra/group.lean
Expand Up @@ -270,7 +270,7 @@ begin
end

@[to_additive]
lemma topological_group.of_nhds_one {G : Type*} [group G] [topological_space G]
lemma topological_group.of_nhds_one {G : Type u} [group G] [topological_space G]
(hmul : tendsto (uncurry ((*) : G → G → G)) ((𝓝 1) ×ᶠ 𝓝 1) (𝓝 1))
(hinv : tendsto (λ x : G, x⁻¹) (𝓝 1) (𝓝 1))
(hleft : ∀ x₀ : G, 𝓝 x₀ = map (λ x, x₀*x) (𝓝 1))
Expand Down

0 comments on commit b1aafb2

Please sign in to comment.