mathlib3

0ab9b5f3 - chore(topology/continuous_function/bounded): golf algebra instances (#12082)

chore(topology/continuous_function/bounded): golf algebra instances (#12082) Using the `function.injective.*` lemmas saves a lot of proofs. This also adds a few missing lemmas about `one` that were already present for `zero`.