Commit 2024-10-01 05:27 0da2361b

View on Github →

chore: tidy various files (#17095)

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

Modified Mathlib/Algebra/Lie/Subalgebra.lean

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

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

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

Modified Mathlib/FieldTheory/Finiteness.lean

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/Logic/Function/FiberPartition.lean

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

Modified Mathlib/MeasureTheory/Measure/SeparableMeasure.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

modified theorem NumberField.mixedEmbedding.fundamentalCone.integralPoint_ne_zero

Modified Mathlib/Probability/Distributions/Gamma.lean

Modified Mathlib/RingTheory/MvPowerSeries/LexOrder.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

Modified Mathlib/Topology/FiberPartition.lean