radius_compContinuousLinearMap_eq

English

Radius respects homogeneous linear structure: multiplying all coefficients by a common scalar does not alter the radius.

Русский

Радиус сохраняется при однородном линейном преобразовании коэффициентов.

LaTeX

$$$\\forall c,\\ radius(c\\cdot p) = radius(p)$.$$

Lean4

/-- This is a version of `radius_compContinuousLinearMap_linearIsometryEquiv_eq` with better
opportunity for unification, at the cost of manually supplying some hypotheses. -/
theorem radius_compContinuousLinearMap_eq [Nontrivial E] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F)
    (hu_iso : Isometry u) (hu_surj : Function.Surjective u) : (p.compContinuousLinearMap u).radius = p.radius :=
  let v : E ≃ₗᵢ[𝕜] F :=
    { LinearEquiv.ofBijective u.toLinearMap ⟨hu_iso.injective, hu_surj⟩ with
      norm_map' := hu_iso.norm_map_of_map_zero (map_zero u) }
  radius_compContinuousLinearMap_linearIsometryEquiv_eq p v

Похожие утверждения