Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7095,6 +7095,7 @@ public import Mathlib.Tactic.Contrapose
public import Mathlib.Tactic.Conv
public import Mathlib.Tactic.Convert
public import Mathlib.Tactic.Core
public import Mathlib.Tactic.CrossRefAttribute
public import Mathlib.Tactic.DSimpPercent
public import Mathlib.Tactic.DeclarationNames
public import Mathlib.Tactic.DefEqAbuse
Expand Down Expand Up @@ -7311,7 +7312,6 @@ public import Mathlib.Tactic.Simps.Basic
public import Mathlib.Tactic.Simps.NotationClass
public import Mathlib.Tactic.SplitIfs
public import Mathlib.Tactic.Spread
public import Mathlib.Tactic.StacksAttribute
public import Mathlib.Tactic.Subsingleton
public import Mathlib.Tactic.Substs
public import Mathlib.Tactic.SuccessIfFailWithMsg
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Ring/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@ module

public import Mathlib.Algebra.GroupWithZero.Defs
public import Mathlib.Data.Int.Cast.Defs
public import Mathlib.Tactic.CrossRefAttribute
public import Mathlib.Tactic.Spread
public import Mathlib.Tactic.StacksAttribute

/-!
# Semirings and rings
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/CategoryTheory/Category/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@ module
public import Mathlib.CategoryTheory.Category.Init
public import Mathlib.Combinatorics.Quiver.Basic
public import Mathlib.Tactic.PPWithUniv
public import Mathlib.Tactic.CrossRefAttribute
public import Mathlib.Tactic.Common
public import Mathlib.Tactic.StacksAttribute
public import Mathlib.Tactic.TryThis

/-!
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,7 @@ public import Mathlib.Tactic.Contrapose
public import Mathlib.Tactic.Conv
public import Mathlib.Tactic.Convert
public import Mathlib.Tactic.Core
public import Mathlib.Tactic.CrossRefAttribute
public import Mathlib.Tactic.DSimpPercent
public import Mathlib.Tactic.DeclarationNames
public import Mathlib.Tactic.DefEqAbuse
Expand Down Expand Up @@ -290,7 +291,6 @@ public import Mathlib.Tactic.Simps.Basic
public import Mathlib.Tactic.Simps.NotationClass
public import Mathlib.Tactic.SplitIfs
public import Mathlib.Tactic.Spread
public import Mathlib.Tactic.StacksAttribute
public import Mathlib.Tactic.Subsingleton
public import Mathlib.Tactic.Substs
public import Mathlib.Tactic.SuccessIfFailWithMsg
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Topology/Irreducible.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@ module
public import Mathlib.Order.Minimal
public import Mathlib.Order.Zorn
public import Mathlib.Topology.ContinuousOn
public import Mathlib.Tactic.StacksAttribute
public import Mathlib.Topology.DiscreteSubset
public import Mathlib.Tactic.CrossRefAttribute

/-!
# Irreducibility in topological spaces
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Topology/JacobsonSpace.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ module

public import Mathlib.Topology.LocalAtTarget
public import Mathlib.Topology.Separation.Regular
public import Mathlib.Tactic.StacksAttribute
public import Mathlib.Tactic.CrossRefAttribute

/-!

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Topology/Separation/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ public import Mathlib.Topology.Piecewise
public import Mathlib.Topology.Separation.SeparatedNhds
public import Mathlib.Topology.Compactness.LocallyCompact
public import Mathlib.Topology.Bases
public import Mathlib.Tactic.StacksAttribute
public import Mathlib.Tactic.CrossRefAttribute

/-!
# Separation properties of topological spaces
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Topology/Separation/Regular.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,10 @@ Authors: Johannes Hölzl, Mario Carneiro
-/
module

public import Mathlib.Tactic.StacksAttribute
public import Mathlib.Topology.Compactness.Lindelof
public import Mathlib.Topology.Separation.Hausdorff
public import Mathlib.Topology.Connected.Clopen
public import Mathlib.Tactic.CrossRefAttribute

/-!
# Regular, normal, T₃, T₄ and T₅ spaces
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Topology/Spectral/Hom.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,9 @@ Authors: Yaël Dillies
-/
module

public import Mathlib.Tactic.StacksAttribute
public import Mathlib.Topology.ContinuousMap.Basic
public import Mathlib.Topology.Maps.Proper.Basic
public import Mathlib.Tactic.CrossRefAttribute

/-!
# Spectral maps
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import Mathlib.Tactic.StacksAttribute
import Mathlib.Tactic.CrossRefAttribute
import Mathlib.Util.ParseCommand

/-- info: No tags found. -/
Expand Down
Loading