Commit 2025-12-08 11:36 cb9a87db
View on Github →doc(Analysis.Normed.Lp.LpEquiv): fix a typo and change two variables (#32491) The doc contained two minor typos. Also, some variables where left explicit because "Lean has elaboration problems", but this is no longer true, and this PR makes them implicit.