referring to namespace in theorem name

Stream: mathlib4

[Patrick Massot]

I have a theorem about Sigma.mk, docs#set.range_sigma_mk. What should be the Lean 4 name: Set.range_sigma_mk or Set.range_sigmaMk or something else?

[Floris van Doorn]

I think we should refer to Foo.bar and Foo.Bar inside lemmas as fooBar (or bar if the namespace is not necessary to include). So I think it should be Set.range_sigmaMk.

[Floris van Doorn]

I came across the same issue in Data.Nat.Cast.Basic with lemmas like theorem op_natCast (n : ℕ) : op (n : α) = n, which seems better to me than op_nat_cast.