Commit 2024-06-29 09:06 0cbe15b9

View on Github →

chore: tidy various files (#14230)

Estimated changes

Modified Mathlib/Algebra/Module/LocalizedModule.lean

Modified Mathlib/Algebra/Polynomial/Smeval.lean

Modified Mathlib/Algebra/Star/StarRingHom.lean

Modified Mathlib/Algebra/Vertex/HVertexOperator.lean

modified theorem VertexAlg.HetVertexOperator.ext

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

Modified Mathlib/CategoryTheory/Sites/OneHypercover.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Data/Matroid/Map.lean

Modified Mathlib/Data/Real/EReal.lean

Modified Mathlib/Data/Real/NNReal.lean

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

Modified Mathlib/Logic/Equiv/Set.lean

Modified Mathlib/Logic/Hydra.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean

Modified Mathlib/NumberTheory/SiegelsLemma.lean

Modified Mathlib/Order/Filter/SmallSets.lean

Modified Mathlib/Order/GameAdd.lean

Modified Mathlib/Order/KrullDimension.lean

Modified Mathlib/RingTheory/Binomial.lean

Modified Mathlib/RingTheory/OreLocalization/Ring.lean

Modified Mathlib/SetTheory/Game/Basic.lean

modified def SetTheory.PGame.mulOption

modified theorem SetTheory.PGame.mulOption_symm

Modified Mathlib/Topology/Instances/NNReal.lean