English
The collection AlgebraNorm R S forms an AlgebraNormClass with compatibility to ring and scalar actions; in particular, map_zero, map_add_le_add, map_mul_le_mul, neg', eq_zero_of_map_eq_zero', and map_smul_eq_mul hold.
Русский
Множество AlgebraNorm R S образует AlgebraNormClass, совместимый с кольцевыми и скалярными операциями; в частности выполняются свойства map_zero, map_add_le_add, map_mul_le_mul, neg', eq_zero_of_map_eq_zero', map_smul_eq_mul.
LaTeX
$$$AlgebraNorm\\,algebraNormClass\\;\\text{(R,S)}$$$
Lean4
instance algebraNormClass : AlgebraNormClass (AlgebraNorm R S) R S
where
map_zero f := f.map_zero'
map_add_le_add f := f.add_le'
map_mul_le_mul f := f.mul_le'
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'
