From bee9b843b839152abe82ced0aeacff96a6c98991 Mon Sep 17 00:00:00 2001 From: Mauricio Collares Date: Fri, 26 May 2023 16:07:16 +0200 Subject: [PATCH] fix merge --- src/topology/algebra/infinite_sum/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/topology/algebra/infinite_sum/basic.lean b/src/topology/algebra/infinite_sum/basic.lean index bed947c43204b..344b0ba618d35 100644 --- a/src/topology/algebra/infinite_sum/basic.lean +++ b/src/topology/algebra/infinite_sum/basic.lean @@ -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