Commit 2026-08-03 21:26 899f7e5f
View on Github →feat(Topology/Algebra/Module/Spaces/ContinuousLinearMap): convert toLinearMap₁₂ to a linear map (#41731)
Convert the projection toLinearMap₁₂ (which strips the topology from a continuous semibilinear map) to a linear map, by showing that it preserves addition and scalar multiplication. We also rename toLinearMap₁₂_apply to toLinearMap₁₂_apply_apply_apply without deprecation so that we can have _apply be a different lemma.