times_cont_diff name

Stream: maths

[Patrick Massot]

I know this has already been discussed, but I can't find the messages. I think we really need a shorter name for times_cont_diff. Using notations is not enough, this appears in a lot of lemma names. I've just spent two hours proving differentiability lemmas in the sphere eversion project and I have many more to prove. This is simply too long. I don't want something completely obscure like tcd but maybe we could at least remove the times_? @Sebastien Gouezel @Yury G. Kudryashov

[Yury G. Kudryashov]

What about smooth? I know that it is currently used in manifolds. I don't mind writing msmooth ∞ instead of smooth there.

[Patrick Massot]

smooth would sound weird for finite n

[Floris van Doorn]

maybe is_C, so is_C 𝕜 n f corresponds to $f \in C^n$.
Probably to cryptic though.

[Heather Macbeth]

I think cont_diff sounds reasonable, indeed.

[Sebastien Gouezel]

Yes, cont_diff looks ok.

[Yaël Dillies]

I personally could never make the meaning times in this name. Is it "continuous differentiable that many times"? I thought it could also refer to`× somehow.

[Patrick Massot]

@Yury G. Kudryashov are you also ok with cont_diff?

[Patrick Massot]

If yes then I'll try to open a PR so that someone can merge it really fast. It should be as easy as a global search and replace.

[Patrick Massot]

VScode says times_cont_diff appears 1987 times in 31 files.

[Patrick Massot]

And add 799 hits for times_cont_mdiff

[Damiano Testa]

Surely nothing can go wrong when changing 2786 names in 31 files...

[Patrick Massot]

I opened #12227 without waiting for Yury's answer since creating the PR was very little work.

[Yury G. Kudryashov]

Thank you! I was away from computer for some time.