English
The induced NormedAlgebra structure ensures ‖f(a b)‖ ≤ ‖a‖ · ‖f(b)‖ for a non-unital AlgHom f.
Русский
Индукцированная структура NormedAlgebra обеспечивает неравенство ‖f(a b)‖ ≤ ‖a‖ · ‖f(b)‖ для невзаимной алгебраической гомоморфной карты f.
LaTeX
$$$\\|f(a b)\\| \\le \\|a\\| \\cdot \\|f(b)\\|$$$
Lean4
/-- A non-unital algebra homomorphism from an `Algebra` to a `NormedAlgebra` induces a
`NormedAlgebra` structure on the domain, using the `SeminormedRing.induced` norm.
See note [reducible non-instances] -/
abbrev induced {F : Type*} (𝕜 R S : Type*) [NormedField 𝕜] [Ring R] [Algebra 𝕜 R] [SeminormedRing S] [NormedAlgebra 𝕜 S]
[FunLike F R S] [NonUnitalAlgHomClass F 𝕜 R S] (f : F) : @NormedAlgebra 𝕜 R _ (SeminormedRing.induced R S f) :=
letI := SeminormedRing.induced R S f
⟨fun a b ↦ show ‖f (a • b)‖ ≤ ‖a‖ * ‖f b‖ from (map_smul f a b).symm ▸ norm_smul_le a (f b)⟩
