Commit 2026-03-06 09:45 ab0ddc2e

refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs (#35567) This PR cleans up the proofs in Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean} In addition, it performs the following minor structural changes:

• Weaken assumptions from NontriviallyNormedField 𝕜 to NormedField 𝕜 where possible
• The proofs showing that projectiveSeminorm actually defines a Seminorm are split off into separate lemmas. This mimics the idiom used e.g. in Analysis.Normed.Modula.Operator.Basic to define the operator norm.
• Register a Nonempty x.lifts instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances. This is the first in a series of three PRs with the goal to deprecate PiTensorProuduct.injectiveSeminorm.