Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-03 16:00
7305307d
View on Github →
chore: tidy various files (
#21367
)
Estimated changes
Modified
Mathlib/Algebra/Algebra/Basic.lean
Modified
Mathlib/Algebra/CharP/LinearMaps.lean
Modified
Mathlib/Algebra/Group/Subgroup/Basic.lean
Modified
Mathlib/Algebra/Module/CharacterModule.lean
Modified
Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
Modified
Mathlib/Algebra/Order/GroupWithZero/Bounds.lean
Modified
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
modified
theorem
MonotoneOn.mul
Modified
Mathlib/Algebra/Polynomial/Div.lean
Modified
Mathlib/Algebra/Ring/Parity.lean
Modified
Mathlib/Algebra/Ring/Subsemiring/Basic.lean
Modified
Mathlib/Analysis/MeanInequalities.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
Modified
Mathlib/CategoryTheory/Shift/Opposite.lean
Modified
Mathlib/CategoryTheory/Shift/Pullback.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Clique.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Path.lean
Modified
Mathlib/Data/DFinsupp/Small.lean
Modified
Mathlib/Data/ENNReal/Operations.lean
Modified
Mathlib/Data/List/ReduceOption.lean
Modified
Mathlib/Data/Multiset/Basic.lean
Modified
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
Modified
Mathlib/LinearAlgebra/Basis/Exact.lean
Modified
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
Modified
Mathlib/NumberTheory/Cyclotomic/Basic.lean
Modified
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
modified
theorem
DedekindDomain.FiniteAdeleRing.coe_add
modified
theorem
DedekindDomain.FiniteAdeleRing.coe_algebraMap
modified
theorem
DedekindDomain.FiniteAdeleRing.coe_mul
deleted
theorem
DedekindDomain.FiniteAdeleRing.coe_zero:
added
theorem
DedekindDomain.FiniteAdeleRing.coe_zero
Modified
Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean
modified
def
ProfiniteGrp.toFiniteQuotientFunctor
Modified
Mathlib/Topology/Algebra/LinearTopology.lean
Modified
Mathlib/Topology/Algebra/Module/ModuleTopology.lean
Modified
Mathlib/Topology/PartialHomeomorph.lean