Commit 2024-07-09 09:58 fa8a27fd

View on Github →

chore: remove superfluous open statements (#14543) Not exhaustive: hand-minimized in a few selected files

Estimated changes

Modified Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean

Modified Mathlib/Analysis/Distribution/FourierSchwartz.lean

Modified Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

Modified Mathlib/CategoryTheory/Idempotents/Karoubi.lean

Modified Mathlib/Combinatorics/Additive/Dissociation.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/GroupTheory/Congruence/BigOperators.lean

Modified Mathlib/LinearAlgebra/Matrix/Permutation.lean

Modified Mathlib/MeasureTheory/Function/Intersectivity.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified Mathlib/Probability/BorelCantelli.lean

Modified Mathlib/RingTheory/Congruence/BigOperators.lean

Modified Mathlib/RingTheory/Flat/EquationalCriterion.lean

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

Modified Mathlib/Topology/ContinuousFunction/CompactlySupported.lean