Commit 2024-11-29 19:27 f9e900aa

View on Github →

chore(Filter/Prod): drop Filter.prod, use SProd instead (#18315) This way we can't accidentally use the underlying Filter.prod instead of the normal form.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean

Modified Mathlib/Data/Analysis/Filter.lean

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.eventually_imp_distrib_left

added theorem Filter.frequently_and_distrib_left

added theorem Filter.frequently_and_distrib_right

Modified Mathlib/Order/Filter/Curry.lean

modified theorem Filter.curry_le_prod

modified theorem Filter.eventually_curry_iff

modified theorem Filter.eventually_curry_prod_iff

modified theorem Filter.frequently_curry_iff

modified theorem Filter.frequently_curry_prod_iff

modified theorem Filter.mem_curry_iff

modified theorem Filter.prod_mem_curry

Modified Mathlib/Order/Filter/Defs.lean

Modified Mathlib/Order/Filter/Finite.lean

deleted theorem Filter.eventually_imp_distrib_left

deleted theorem Filter.frequently_and_distrib_left

deleted theorem Filter.frequently_and_distrib_right

Modified Mathlib/Order/Filter/Prod.lean

Modified Mathlib/Topology/Algebra/UniformGroup/Defs.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/Instances/TrivSqZeroExt.lean

modified theorem TrivSqZeroExt.nhds_def

modified theorem TrivSqZeroExt.nhds_inl

modified theorem TrivSqZeroExt.nhds_inr

Modified Mathlib/Topology/UniformSpace/Basic.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergence.lean

deleted theorem TendstoUniformlyOn.prod