Commit 2023-12-04 22:16 397ec08b

View on Github →

chore: tidy various files (#8818)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Free.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

Modified Mathlib/Analysis/NormedSpace/Pointwise.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

modified theorem Complex.Gamma_one

Modified Mathlib/Analysis/SpecialFunctions/Gaussian.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Base.lean

Modified Mathlib/CategoryTheory/Limits/Fubini.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Ulift.lean

Modified Mathlib/Control/Traversable/Equiv.lean

added theorem Equiv.traverse_def

Modified Mathlib/Data/DFinsupp/Basic.lean

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Data/Int/ModEq.lean

Modified Mathlib/Data/Int/Parity.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/Rel.lean

Modified Mathlib/FieldTheory/Normal.lean

Modified Mathlib/FieldTheory/NormalClosure.lean

Modified Mathlib/GroupTheory/Order/Min.lean

Modified Mathlib/GroupTheory/PushoutI.lean

Modified Mathlib/GroupTheory/Torsion.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

Modified Mathlib/MeasureTheory/Constructions/HaarToSphere.lean

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Probability/Distributions/Exponential.lean

Modified Mathlib/Probability/Independence/Kernel.lean

Modified Mathlib/Topology/Basic.lean

Modified Mathlib/Topology/CompletelyRegular.lean

Modified Mathlib/Topology/MetricSpace/Infsep.lean