New name for Nat.cast n • x = n • x

Stream: mathlib4

[Yaël Dillies]

#14997 renames (and turns around) docs#nsmul_eq_smul_cast to natCast_smul_eq_nsmul. Are people happy with this new name or do they want another one?

[Yaël Dillies]

/poll What name to use?
natCast_smul_eq_nsmul
Nat.cast_smul_eq_nsmul

[Eric Wieser]

Maybe there's a #naming rule here that Foo.foo x <op> Bar.bar should be called fooFoo_op_barBar and never Foo.foo_op_barBar, since the head symbol is really op?

[Eric Wieser]

(but that rule doesn't work for docs#Prod.mk_add_mk !)

[Yaël Dillies]

Eric Wieser said:

Maybe there's a #naming rule here that Foo.foo x <op> Bar.bar should be called fooFoo_op_barBar and never Foo.foo_op_barBar, since the head symbol is really op?

Maybe, but I doubt this applies here. Both Nat.cast and nsmul are about Nat

[Yaël Dillies]

I've changed to Nat.cast_smul_eq_nsmul/Int.cast_smul_eq_zsmul. I will merge now