Theorem ContinuousMultilinearMap.continuous_precomp

Modification history

2026-05-25 09:15
Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
feat(Topology/Algebra/Module): call `eta_expand` in the default tactic of `ContinuousLinearEquiv` (#39766) …
Added ContinuousMultilinearMap.continuous_precompView on Github →