Commit 2023-05-29 10:13 46aa58dc

View on Github →

chore: tidy various files (#4466)

Estimated changes

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

Modified Mathlib/Analysis/NormedSpace/FiniteDimension.lean

Modified Mathlib/CategoryTheory/Abelian/Projective.lean

Modified Mathlib/Geometry/Euclidean/Sphere/Basic.lean

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

modified theorem charmatrix_apply_natDegree_le

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean

added theorem MulChar.equivToUnitHom_symm_coe

deleted theorem MulChar.equiv_unit_hom_symm_coe

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

added theorem PadicInt.norm_sub_modPart_aux

deleted theorem PadicInt.norm_sub_mod_part_aux

Modified Mathlib/RingTheory/Ideal/LocalRing.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/JacobsonIdeal.lean

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

added theorem LinearEquiv.coe_toContinuousLinearEquiv'

deleted theorem LinearEquiv.coe_to_continuous_linear_equiv'

added theorem LinearMap.coe_toContinuousLinearMap'

deleted theorem LinearMap.coe_to_continuous_linear_map'

Modified Mathlib/Topology/Category/TopCommRingCat.lean

Modified Mathlib/Topology/Sheaves/Sheaf.lean

deleted def TopCat.Presheaf.IsSheaf

deleted def TopCat.Sheaf

Modified Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean