Zulip Chat Archive

Stream: mathlib4

Topic: Naming `LinearMap.toMatrix'_toLin'` etc

Yury G. Kudryashov (May 09 2025 at 14:18):

Should docs#LinearMap.toMatrix'_toLin' which says (M : Matrix ..) : M.toLin'.toMatrix' = M be in the LinearMap or in the Matrix namespace?

Yury G. Kudryashov (May 09 2025 at 14:19):

It's about LinearMap.toMatrix', Matrix.toLin', and (M : Matrix ..).

Last updated: Dec 20 2025 at 21:32 UTC