mathlib

aa666983 - feat(topology/algebra/module/star): continuity results for star_modules (#19037)

feat(topology/algebra/module/star): continuity results for star_modules (#19037) Notably this adds `starL`. This also fixes some unnecessary typeclass arguments in `star_linear_equiv`. Co-authored-by: ADedecker <anatolededecker@gmail.com>