Commit 2025-02-09 07:10 e05e2250

View on Github →

chore: tidy various files (#21568)

Estimated changes

Modified Archive/Imo/Imo1982Q1.lean

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/BrauerGroup/Defs.lean

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

modified theorem MonoidAlgebra.lsingle_apply

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

modified theorem Polynomial.eq_zero_of_mul_eq_zero_of_smul

Modified Mathlib/AlgebraicGeometry/RationalMap.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Defs.lean

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

Modified Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean

Modified Mathlib/Combinatorics/SimpleGraph/Sum.lean

Modified Mathlib/FieldTheory/Minpoly/IsConjRoot.lean

Modified Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

Modified Mathlib/ModelTheory/Semantics.lean

Modified Mathlib/NumberTheory/LSeries/Positivity.lean

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

modified theorem NumberField.mixedEmbedding.disjoint_negAt_plusPart

modified theorem NumberField.mixedEmbedding.negAt_preimage

modified theorem NumberField.mixedEmbedding.pos_of_not_mem_negAt_plusPart

Modified Mathlib/NumberTheory/Ostrowski.lean

Modified Mathlib/Order/Nucleus.lean

Modified Mathlib/Order/TransfiniteIteration.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

modified def HahnSeries.SummableFamily.smul

Modified Mathlib/RingTheory/LaurentSeries.lean

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