Commit 2021-03-26 22:21 ca7dca39
View on Github →feat(geometry/manifold/algebra/smooth_functions): simp lemmas for coercions to functions (#6893)
These came up while working on the branch replace_algebra_def but seem worth adding
in their own right.