Commit 2021-07-03 09:58 915902e6

View 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 dfinsupp.

Estimated changes