mathlib

915902e6 - feat(topology/algebra/multilinear): add a linear_equiv version of pi (#8064)

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`.