Commit 2024-02-02 21:55 4b37d531

View on Github →

chore: tidy various files (#10007)

Estimated changes

Modified Mathlib/Computability/RegularExpressions.lean

Modified Mathlib/Data/List/BigOperators/Basic.lean

Modified Mathlib/Data/ZMod/Module.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

Modified Mathlib/Order/Filter/NAry.lean

Modified Mathlib/RingTheory/Filtration.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean

modified theorem isLindelof_empty