Zulip Chat Archive

Stream: general

Topic: scalar smul naming discrepancy

Bernd Losert (May 30 2022 at 21:03):

I'm noticing some discrepancy in the naming. For example, you have has_scalar and has_faithful_scalar, but you have has_continuous_smul, has_bounded_smul, has_measurable_smul. I wonder if there's some rationale here.

Eric Wieser (May 30 2022 at 21:27):

I think there's a past thread on this but I won't look for it on mobile. Search for has_smul?

Eric Wieser (May 30 2022 at 21:28):

I think a rename was marginally favored

Bernd Losert (May 30 2022 at 21:47):

Can't find it.

Julian Berman (May 30 2022 at 21:55):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/left.20vs.20right.20modules.20in.20tensor.20products/near/261976176 maybe

Eric Wieser (May 31 2022 at 09:56):

Looks like support was fairly unanimous

Eric Wieser (May 31 2022 at 09:56):

I recommend renaming has_faithful_scalar first just to keep the size of the diff down

Bernd Losert (Jun 02 2022 at 15:25):

Eric Wieser said:

I recommend renaming has_faithful_scalar first just to keep the size of the diff down

I have the branch ready. What title should I use for the pull request?

Bernd Losert (Jun 02 2022 at 17:20):

PR: https://github.com/leanprover-community/mathlib/pull/14515

Violeta Hernández (Jun 02 2022 at 17:39):

We aren't all that strict with PR names

Eric Wieser (Jun 02 2022 at 18:08):

One thing for next time; don't delete the PR template message, as it includes a gitpod link that can be useful to reviewers

Yury G. Kudryashov (Jun 05 2022 at 01:44):

On the queue

Bernd Losert (Jun 05 2022 at 10:03):

It was merged. Nice. Here's the next PR:
https://github.com/leanprover-community/mathlib/pull/14559

Eric Wieser (Jun 05 2022 at 11:19):

Is the plan to leave is_central_scalar and is_scalar_tower untouched?

Bernd Losert (Jun 05 2022 at 11:23):

I was wondering the same thing. I could make another PR for those.

Eric Wieser (Jun 05 2022 at 11:26):

I'd wait for more opinions on those two

Eric Wieser (Jun 05 2022 at 11:27):

(also note that your PR fails CI)

Bernd Losert (Jun 05 2022 at 17:29):

I think it's good now.

Bernd Losert (Jun 11 2022 at 20:41):

Bump: https://github.com/leanprover-community/mathlib/pull/14559
@Eric Wieser

Bernd Losert (Jun 29 2022 at 08:43):

@Yury G. Kudryashov
I updated the branch: https://github.com/leanprover-community/mathlib/pull/14559#issuecomment-1167916032

Yury G. Kudryashov (Jun 29 2022 at 12:09):

merged master again, delegated. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC