Commit 2023-09-12 22:27 ac0ad1e8

View on Github →

chore: tidy various files (#7081)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finprod.lean

deleted theorem MonoidHom.map_finprod_pLift

added theorem MonoidHom.map_finprod_plift

deleted theorem finprod_eq_prod_pLift_of_mulSupport_subset

deleted theorem finprod_eq_prod_pLift_of_mulSupport_toFinset_subset

added theorem finprod_eq_prod_plift_of_mulSupport_subset

added theorem finprod_eq_prod_plift_of_mulSupport_toFinset_subset

modified theorem finprod_eq_single

Modified Mathlib/Analysis/Convex/Combination.lean

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

Modified Mathlib/Geometry/Manifold/BumpFunction.lean

Modified Mathlib/Order/Filter/Bases.lean

added theorem Filter.HasBasis.to_hasBasis'

deleted theorem Filter.HasBasis.to_has_basis'

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean