Commit 2025-04-24 05:39 a6a1efc4

View on Github →

chore: tidy various files (#24331)

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Polynomial/Laurent.lean

modified theorem LaurentPolynomial.mk'_eq

modified theorem LaurentPolynomial.mk'_one_X

modified theorem LaurentPolynomial.mk'_one_X_pow

Modified Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Pi.lean

Modified Mathlib/Analysis/Complex/Periodic.lean

Modified Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

Modified Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

Modified Mathlib/Combinatorics/SimpleGraph/Diam.lean

Modified Mathlib/Data/Matroid/Minor/Order.lean

Modified Mathlib/Data/Nat/Init.lean

Modified Mathlib/Data/PNat/Factors.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean

Modified Mathlib/LinearAlgebra/Matrix/Ideal.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Quotient.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/L1.lean

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/NumberTheory/NumberField/Completion.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

modified theorem RatFunc.single_one_eq_pow