Commit 2023-02-09 19:18 8c8c544b

chore(topology/algebra): make the divisor argument of div_const explicit (#18411) This is using the rule "parameters which do not appear in the types of other parameters should be explicit". In particular, this means that it is easier to use proofs of the form convert hf.div_const c, without having to omit c and hope that Lean can guess it. This makes the argument explicit for:

• cont_diff_within_at.div_const
• cont_diff_at.div_const
• cont_diff_on.div_const
• cont_diff.div_const
• filter.tendsto.div_const
• continuous_at.div_const
• continuous_within_at.div_const
• continuous_on.div_const
• continuous.div_const
• differentiable_within_at.div_const
• differentiable_at.div_const
• differentiable_on.div_const
• differentiable.div_const
• deriv_within_div_const It was already explicit for:
• filter.tendsto.div_const'
• has_sum.div_const
• summable.div_const
• integrable.div_const
• has_deriv_at.div_const
• has_deriv_within_at.div_const
• has_strict_deriv_at.div_const
• periodic.div_const
• measurable.div_const
• ae_measurable.div_const
• The mul variants of many of the above