Commit 2025-07-30 09:29 36bd1b9d
View on Github →refactor: Rename ContinuousLinearMap.toLinearMap₂ (#27574)
Rename ContinuousLinearMap.toLinearMap₂ to ContinuousLinearMap.toLinearMap₁₂.
See the discussion here: https://github.com/leanprover-community/mathlib4/pull/26345#pullrequestreview-3059683061