Commit 2023-09-08 15:47 d04897a6

View on Github →

chore: tidy various files (#7035)

Estimated changes

Modified Mathlib/Algebra/Group/OrderSynonym.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

Modified Mathlib/Algebra/Homology/QuasiIso.lean

Modified Mathlib/Algebra/Order/Group/Instances.lean

Modified Mathlib/Algebra/Order/Monoid/OrderDual.lean

Modified Mathlib/Algebra/Order/SMul.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion/Scheme.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

Modified Mathlib/Data/ENat/Lattice.lean

modified theorem ENat.iInf_coe_ne_top

Modified Mathlib/Data/Rat/Cast/Order.lean

added theorem Rat.castHom_rat

deleted theorem Rat.cast_hom_rat

Modified Mathlib/Data/Sum/Basic.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

deleted theorem Matrix.isUnit_charpolyRev_of_IsNilpotent

added theorem Matrix.isUnit_charpolyRev_of_isNilpotent

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

deleted theorem IsFiniteMeasure.lintegral_lt_top_of_bounded_to_eNNReal

added theorem IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

Modified Mathlib/NumberTheory/RamificationInertia.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Order/SuccPred/Basic.lean

modified theorem Order.succ_le_succ_iff_of_not_isMax

modified theorem Order.succ_lt_succ_iff_of_not_isMax

Modified Mathlib/RingTheory/Ideal/Over.lean

added def Ideal.Quotient.algebraQuotientOfLEComap

deleted def Ideal.Quotient.algebraQuotientOfLeComap

Modified Mathlib/RingTheory/Perfection.lean

Modified Mathlib/Topology/NoetherianSpace.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean

added theorem TopCat.Presheaf.germ_stalkSpecializes'

deleted theorem TopCat.Presheaf.germ_stalk_specializes'

Modified scripts/nolints.json