Theorem NormedSpace.restrictScalars_eq

Modification history

2025-10-07 15:26
Mathlib/Analysis/Normed/Module/Basic.lean
feat: define `curveIntegral` (#24754) …
Added NormedSpace.restrictScalars_eqView on Github →