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: Dec 20 2023 at 11:08 UTC