times_cont_diff): rename `linear_isometry_map.times_cont_diff`; drop `_map` (#10155)

Commit

4 years ago

chore(analysis/calculus/times_cont_diff): rename `linear_isometry_map.times_cont_diff`; drop `_map` (#10155) I think the old name is a typo; the new name enables dot notation.

Author

ocfnash

Parents

3cbe0feb

mathlib3 b8908367 - chore(analysis/calculus/times_cont_diff): rename `linear_isometry_map.times_cont_diff`; drop `_map` (#10155)

mathlib3
b8908367 - chore(analysis/calculus/times_cont_diff): rename `linear_isometry_map.times_cont_diff`; drop `_map` (#10155)