English
If E is a vector space with two scalar structures 𝕜 and 𝕜′ related by an IsScalarTower, and E is equipped with norms making it a NormedSpace over both 𝕜 and 𝕜′, then the NormedSpace structure obtained by restricting scalars from 𝕜 to 𝕜′ coincides with the given 𝕜′-NormedSpace structure.
Русский
Если у пространства E есть две структуры скаляров 𝕜 и 𝕜′, связанные тождением IsScalarTower, и на E задана норма так, что E является NormedSpace над 𝕜 и над 𝕜′, то полученная структура NormedSpace при ограничении скаляров совпадает с данной структурой над 𝕜′.
LaTeX
$$$${\rm NormedSpace}_{\mathbb{K},\mathbb{K}'}(E) = h,$$ где ограничение скаляров совпадает с исходной структурой.$$
Lean4
theorem restrictScalars_eq {E : Type*} [SeminormedAddCommGroup E] [h : NormedSpace 𝕜 E] [NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E] : NormedSpace.restrictScalars 𝕜 𝕜' E = h :=
by
ext
apply algebraMap_smul
