mathlib

8c8c544b - chore(topology/algebra): make the divisor argument of `div_const` explicit (#18411)

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