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 ContinuousLinearMap.continuous_postcomp_continuousMultilinearMap