mulAlgebraNormClass — Mathlib

English

Two MulAlgebraNorms are equal if they agree on all elements; extensionality principle for MulAlgebraNorm.

Русский

Две MulAlgebraNorm равны, если они совпадают на всех элементах; принцип экстенсивности MулAlgebraNorm.

LaTeX

$$$\\forall p,q:\\ MulAlgebraNorm\\,R\\,S: (\\forall x:\\ S, p\\ x = q\\ x)\\Rightarrow p=q$$$

Lean4

instance mulAlgebraNormClass : MulAlgebraNormClass (MulAlgebraNorm R S) R S
    where
  map_zero f := f.map_zero'
  map_add_le_add f := f.add_le'
  map_one f := f.map_one'
  map_mul f := f.map_mul'
  map_neg_eq_map f := f.neg'
  eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _
  map_smul_eq_mul f := f.smul'

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