Commit 2024-03-19 20:08 b3a2821f

View on Github →

chore: tidy various files (#11490)

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom.lean

modified def AlgHomClass.toAlgHom

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

modified theorem AlgHom.ker_rangeRestrict

modified theorem AlgHom.rangeRestrict_surjective

Modified Mathlib/Algebra/Module/CharacterModule.lean

Modified Mathlib/Algebra/Order/Nonneg/Ring.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

Modified Mathlib/Combinatorics/SetFamily/Shadow.lean

modified theorem Finset.mem_shadow_iff_insert_mem

Modified Mathlib/Data/Finset/Preimage.lean

Modified Mathlib/Data/Int/Order/Basic.lean

modified theorem Nat.cast_natAbs

Modified Mathlib/Data/SetLike/Basic.lean

Modified Mathlib/FieldTheory/PurelyInseparable.lean

Modified Mathlib/GroupTheory/Perm/Basic.lean

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Basic.lean

Modified Mathlib/NumberTheory/Harmonic/Defs.lean

modified theorem harmonic_eq_sum_Icc

modified theorem harmonic_pos

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/Order/Partition/Finpartition.lean

Modified Mathlib/Order/SupIndep.lean

Modified Mathlib/Order/ZornAtoms.lean

Modified Mathlib/RingTheory/Algebraic.lean

Modified Mathlib/RingTheory/Ideal/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

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

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

Modified Mathlib/Topology/Algebra/Module/LinearPMap.lean

Modified Mathlib/Topology/Baire/CompleteMetrizable.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/MetricSpace/Closeds.lean