mathlib
9b2755b9 - chore(*): add missing `to_fun → apply` configurations for `simps` (#15112)

Commit

3 years ago

chore(*): add missing `to_fun → apply` configurations for `simps` (#15112) This improves the names of some generated lemmas for `continuous_map` and `quadratic_form`.

Author

eric-wieser

Parents

ab99fd1b

mathlib 9b2755b9 - chore(*): add missing `to_fun → apply` configurations for `simps` (#15112)

mathlib
9b2755b9 - chore(*): add missing `to_fun → apply` configurations for `simps` (#15112)