Commit 2024-08-06 08:16 26fa8d86

View on Github →

chore: tidy various files (#15516)

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap/Polynomial.lean

Modified Mathlib/Algebra/Module/Zlattice/Basic.lean

Modified Mathlib/Algebra/Module/Zlattice/Covolume.lean

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

Modified Mathlib/Algebra/Order/Group/Unbundled/Abs.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

Modified Mathlib/Algebra/Order/Interval/Basic.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/Analysis/Analytic/Within.lean

Modified Mathlib/Analysis/LocallyConvex/Barrelled.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean

Modified Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean

Modified Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

Modified Mathlib/Data/Matrix/Basis.lean

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/Data/Set/Finite.lean

modified theorem Set.Finite.preimage'

Modified Mathlib/Data/TypeVec.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/GroupTheory/CosetCover.lean

Modified Mathlib/GroupTheory/PGroup.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

Modified Mathlib/Probability/ConditionalProbability.lean

Modified Mathlib/Probability/Kernel/Basic.lean

Modified Mathlib/RingTheory/Finiteness.lean

Modified Mathlib/RingTheory/Flat/Stability.lean

Modified Mathlib/RingTheory/Kaehler/CotangentComplex.lean

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Modified Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

Modified Mathlib/RingTheory/PrimeSpectrum.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean