Commit 2026-06-18 10:58 17367c79

refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): deprecate injectiveSeminorm (#35569) This PR:

• Deprecates PiTensorProduct.injectiveSeminorm and supporting lemmas.
• Moves the theory of liftEquiv from InjectiveSeminorm.lean to ProjectiveSeminorm.lean. No changes are introduced beyond adding deprecation notices, adapting docstrings, and moving material between files. The PR leaves InjectiveSeminorm.lean almost empty. A new implementation of injectiveSeminorm, one which reflects the common mathematical definition, is to be done. This is the third in a series of three PRs with the goal to deprecate PiTensorProuduct.injectiveSeminorm.