Commit 2025-02-14 21:47 ca14452e

View on Github →

chore: tidy various files (#21872)

Estimated changes

Modified Mathlib/Algebra/Azumaya/Basic.lean

deleted theorem IsAzumaya.coe_tensorEquivEnd:

added theorem IsAzumaya.coe_tensorEquivEnd

modified theorem IsAzumaya.mulLeftRight_comp_congr

Modified Mathlib/Algebra/Azumaya/Matrix.lean

deleted theorem AlgHom.mulLeftRightMatrix.comp_inv:

added theorem AlgHom.mulLeftRightMatrix.comp_inv

deleted theorem AlgHom.mulLeftRightMatrix.inv_comp:

added theorem AlgHom.mulLeftRightMatrix.inv_comp

Modified Mathlib/Algebra/Category/Ring/Adjunctions.lean

Modified Mathlib/Algebra/Central/Defs.lean

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

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

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

Modified Mathlib/Algebra/Lie/Abelian.lean

Modified Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean

Modified Mathlib/Algebra/Polynomial/Expand.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf.lean

Modified Mathlib/Analysis/Meromorphic/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean

Modified Mathlib/CategoryTheory/Grothendieck.lean

Modified Mathlib/Data/Int/Defs.lean

Modified Mathlib/Data/List/SplitOn.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/Matroid/Circuit.lean

Modified Mathlib/Data/Set/Monotone.lean

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/FieldTheory/PerfectClosure.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean

Modified Mathlib/GroupTheory/Divisible.lean

Modified Mathlib/GroupTheory/GroupAction/Iwasawa.lean

Modified Mathlib/GroupTheory/GroupAction/Primitive.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Pi.lean

Modified Mathlib/Logic/Equiv/Fin.lean

Modified Mathlib/MeasureTheory/SetSemiring.lean

Modified Mathlib/NumberTheory/Fermat.lean

Modified Mathlib/NumberTheory/LSeries/SumCoeff.lean

Modified Mathlib/NumberTheory/WellApproximable.lean

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Index.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean

Modified Mathlib/Topology/Algebra/IsOpenUnits.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

Modified Mathlib/Topology/Instances/NNReal/Defs.lean

modified theorem NNReal.coeNNRealReal_zero

Modified Mathlib/Topology/Order/ScottTopology.lean