mathlib

9d013ad8 - doc(analysis/normed_space/pi_Lp): fix corrupt synchronization header (#19134)

doc(analysis/normed_space/pi_Lp): fix corrupt synchronization header (#19134) The missing blank line makes a mess in doc-gen. Hopefully this file was just strangely formatted, and this isn't a new bug in the script.