Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
fix merge
Browse files Browse the repository at this point in the history
  • Loading branch information
@collares
collares committed May 26, 2023
1 parent cf248b1 commit bee9b84
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/topology/algebra/infinite_sum/basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1120,7 +1120,7 @@ h.comp_injective $ λ c₁ c₂ h, (prod.ext_iff.1 h).2

section loc_instances
-- enable inferring a T3-topological space from a topological group
local attribute [instance] topological_add_group.t3_space
local attribute [instance] topological_group.t3_space
-- disable getting a T0-space from a T3-space as this causes loops
local attribute [-instance] t3_space.to_t0_space

Expand Down

0 comments on commit bee9b84

Please sign in to comment.