instENormSMulClass — Mathlib

English

Given a normed ring α, a normed space β, and a bilinear action, there is an instance ENormSMulClass α β providing enorm_smul with ENorm.

Русский

Для нормы кольца α и нормированного пространства β существует экземпляр ENormSMulClass α β, задающий enorm_smul.

LaTeX

$$$ENormSMulClass\\;\\alpha\\;\\beta$$$

Lean4

instance (priority := 100) : ENormSMulClass α β where enorm_smul r x := by simp [enorm, nnnorm_smul]

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