instNormOneClassOfNonempty — Mathlib

English

If n is finite and nonempty, and α is a NormOneClass, then Matrix n n α carries a NormOneClass structure.

Русский

Если множество индексов n конечно и непусто, и α обладает NormOneClass, то Matrix n n α имеет структуру NormOneClass.

LaTeX

$$$\text{NormOneClass}(\text{Matrix } n\, n\, α).$$$

Lean4

/-- Note this is safe as an instance as it carries no data. -/
instance [Nonempty n] [DecidableEq n] [One α] [NormOneClass α] : NormOneClass (Matrix n n α) :=
  ⟨(norm_diagonal _).trans <| norm_one⟩

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