Commit 2025-05-29 08:12 914267a5

View on Github →

chore: tidy various files (#25277)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/MvPolynomial/Division.lean

Modified Mathlib/Algebra/MvPolynomial/Rename.lean

Modified Mathlib/Analysis/Asymptotics/LinearGrowth.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/Meromorphic/Divisor.lean

Modified Mathlib/Analysis/Meromorphic/Order.lean

Modified Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean

Modified Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean

Modified Mathlib/Condensed/Light/AB.lean

Modified Mathlib/Data/Complex/Norm.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/Order/Interval/Finset/Box.lean

Modified Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean

Modified Mathlib/RingTheory/Invariant/Profinite.lean

Modified Mathlib/RingTheory/Jacobson/Ring.lean

modified theorem isJacobsonRing_iso

Modified Mathlib/RingTheory/RingHom/Finite.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

Modified Mathlib/SetTheory/PGame/Algebra.lean

Modified Mathlib/SetTheory/PGame/Basic.lean

Modified Mathlib/SetTheory/PGame/Order.lean

Modified Mathlib/Topology/Algebra/ProperAction/Basic.lean

Modified Mathlib/Topology/Exterior.lean