How to name this concept?

Stream: mathlib4

[Ilmārs Cīrulis]

So I've made this PR (#26308) and reviewer suggested that I ask here for the name that's the best for the concept. I have chosen normalized, but maybe the community has better options etc.

import Mathlib.Analysis.RCLike.Basic

/-!
# Normalized vector
Function that calculates unit length vector from a vector
(if the given vector is nonzero vector) or returns zero vector
(if the given vector is zero vector).
-/

variable {V : Type*}
variable [NormedAddCommGroup V]
variable [NormedSpace ℝ V]

/-- The normalized vector from a given vector. `normalized 0 = 0`, otherwise it is
the corresponding unit length vector. -/
noncomputable def normalized (x : V) : V := ‖x‖⁻¹ • x

Thank you :heart:

[Kyle Miller]

normalize is what some other languages use.

Lean seems to use imperative instead of past tense for operations (e.g. add instead of added or addedTo), or sometimes a noun (closure).

[Kyle Miller]

One of the few libraries I found that used normalized is Eigen (for C++), where v.normalize() is for in-place modification and v.normalized() returns a new normalized vector.

[Ilmārs Cīrulis]

Yes, now that you have said that, normalize seems to be better. :thumbs_up:

[Ilmārs Cīrulis]

I changed the name to normalize for now, but now CI fails with this error:
https://github.com/leanprover-community/mathlib4/actions/runs/16609624307/job/46989795171?pr=26308#step:33:23

Error: error: Mathlib.lean:1:0: import Mathlib.Analysis.NormedSpace.Normalize failed, environment already contains 'normalize' from Mathlib.Algebra.GCDMonoid.Basic

What does that exactly mean? And what's the best way to fix it?

[Aaron Liu]

it means you have a name conflict with docs#normalize

[Aaron Liu]

could we reuse that instead?

[Yaël Dillies]

@Ilmārs Cīrulis, I'm very sure we already have this somewhere, but I can't find it. Most relevant declaration I could find is docs#norm_smul_inv_norm

[Jireh Loreaux]

Really? I was fairly certain we didn't have it.

[Ilmārs Cīrulis]

Aaron Liu said:

could we reuse that instead?

That looks too complex for me to understand, at least for now. :sweat:

[Jireh Loreaux]

@Aaron Liu no, we can't use docs#normalize because you would need a monoid structure on your vector space.

[Aaron Liu]

Maybe you can generalize normalize?

[Kyle Miller]

Maybe there's some notion of a normalization module that could be compatible (using V as a module over the semiring R>=0), but it seems to me that these two concepts just happen to use the same word.

Generalizing it to a normalize typeclass doesn't seem good either. For example, the complex numbers C are a module over both R and C. Normalizing in the R vector space sense means to scale the complex number to the unit circle using a positive real. However, C as a NormalizationMonoid (as a module over itself) normalizes everything to 1 (and it must do so, since everything except for 0 is a unit).

Is there some namespace solution here? I doubt that normalize for normalization monoids should be the only normalize in all of mathlib.

[Ilmārs Cīrulis]

So, no solution for this problem? :melting_face:

Ok, will try to think of some other name.

[Eric Wieser]

NormedSpace.normalize perhaps?

[Ilmārs Cīrulis]

Renamed it such way, but this change failed in Post-Build Step (fork) CI step. At least Build and Lint Style was success, that's more than previously.

Error: Process completed with exit code 3. :looking:

[Bryan Gin-ge Chen]

That should hopefully go away if you merge the master branch into your PR branch.

[Ilmārs Cīrulis]

Okay, I tried to do that, now let's wait and see if that helps. Thank you!

[Ilmārs Cīrulis]

:partying_face: It worked.