Zulip Chat Archive

Stream: mathlib4

Topic: LinearMap.proj

Dagur Asgeirsson (Aug 16 2023 at 22:03):

/poll What should LinearMap.proj be called?
LinearMap.proj
Pi.evalₗ
Pi.evalLinearMap

Dagur Asgeirsson (Aug 16 2023 at 22:04):

The Pi versions would be more consistent with the rest of the library, see the note at docs#LinearMap.proj

Dagur Asgeirsson (Aug 16 2023 at 22:23):

This came up in discussions on #6520 where this inconsistency in naming becomes very clear.

Last updated: May 02 2025 at 03:31 UTC