Commit 2022-02-16 19:16 0ab9b5f3
View on Github →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.