Commit 2025-06-23 13:31 ddf91f15

View on Github →

feat: topology on PiLp (#26261) Add a topology on PiLp, along with a CompleteSpace instance.

Estimated changes

modified theorem PiLp.continuous_equiv
modified theorem PiLp.continuous_equiv_symm