Commit 2024-02-08 13:29 890dba74

View on Github →

chore: tidy various files (#10311)

Estimated changes

Modified Mathlib/Algebra/Associated.lean

Modified Mathlib/Algebra/GroupPower/Basic.lean

Modified Mathlib/Algebra/Module/Submodule/Pointwise.lean

deleted theorem Submodule.mem_set_smul(x

added theorem Submodule.mem_set_smul

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Modified Mathlib/Analysis/Complex/TaylorSeries.lean

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

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

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

Modified Mathlib/Computability/TuringMachine.lean

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.castSucc_lt_succ_iff

modified theorem Fin.pred_one'

modified theorem Fin.succ_le_castSucc_iff

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

Modified Mathlib/Data/Finset/Pointwise.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

Modified Mathlib/Data/Polynomial/Derivative.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve.lean

Modified Mathlib/LinearAlgebra/Basis.lean

Modified Mathlib/MeasureTheory/Covering/VitaliFamily.lean

Modified Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

Modified Mathlib/Order/RelSeries.lean

Modified Mathlib/Probability/Distributions/Geometric.lean

modified def ProbabilityTheory.geometricMeasure

modified def ProbabilityTheory.geometricPMF

modified theorem ProbabilityTheory.geometricPMFRealSum

modified theorem ProbabilityTheory.geometricPMFReal_nonneg

modified theorem ProbabilityTheory.isProbabilityMeasureGeometric

modified theorem ProbabilityTheory.stronglyMeasurable_geometricPMFReal

Modified Mathlib/RingTheory/Ideal/MinimalPrime.lean

modified def minimalPrimes

modified theorem minimalPrimes_eq_minimals

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/MetricSpace/Kuratowski.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean