mathlib

560d1a71 - chore(topology/continuous_function/continuous_map): add missing instances for `continuous_map` (#13717)

chore(topology/continuous_function/continuous_map): add missing instances for `continuous_map` (#13717) This adds instances related to the ring variants, i.e., non-unital, non-associative (semi)rings. To avoid introducing accidental diamonds, this also changes how the existing instances are constructed, such that they now go through the `function.injective.*` definitions.