Commit 2021-07-03 09:58 915902e6View on Github →
feat(topology/algebra/multilinear): add a linear_equiv version of pi (#8064)
This is a weaker version of
continuous_multilinear_map.piₗᵢ that requires weaker typeclasses.
Unfortunately I don't understand why the typeclass system continues not to cooperate here, but I suspect it's the same class of problem that plagues