Commit 2023-05-05 12:24 2215ff4f

View on Github →

chore: tidy various files (#3718)

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Ideal.lean

Modified Mathlib/Analysis/Convex/Topology.lean

Modified Mathlib/Analysis/NormedSpace/Star/Basic.lean

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean

modified def CategoryTheory.Limits.parallelFamily

Modified Mathlib/Data/Fintype/Perm.lean

Modified Mathlib/Data/Set/Pointwise/BigOperators.lean

Modified Mathlib/GroupTheory/MonoidLocalization.lean

Modified Mathlib/LinearAlgebra/Dimension.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/LinearAlgebra/Matrix/ZPow.lean

Modified Mathlib/RingTheory/Localization/Ideal.lean

Modified Mathlib/Topology/Category/Top/Opens.lean

added theorem TopologicalSpace.Opens.infLELeft_apply

added theorem TopologicalSpace.Opens.infLELeft_apply_mk

deleted theorem TopologicalSpace.Opens.infLeLeft_apply

deleted theorem TopologicalSpace.Opens.infLeLeft_apply_mk

Modified Mathlib/Topology/DiscreteQuotient.lean

Modified Mathlib/Topology/Instances/Matrix.lean

Modified Mathlib/Topology/MetricSpace/Polish.lean

Modified Mathlib/Topology/UniformSpace/Separation.lean

Modified Mathlib/Topology/UrysohnsLemma.lean