instMulRingNormClassOfNontrivialOfIsDomain

English

Under suitable assumptions (Nontrivial R and IsDomain S), the pair (AbsoluteValue R S, R, S) endows R with a multiplicative ring norm structure.

Русский

При подходящих условиях (Nontrivial R и IsDomain S) абсолютная величина превращает R в кольцевую норму с мультипликативной нормой.

LaTeX

$$$\\text{MulRingNormClass}(\\operatorname{AbsoluteValue} R S, R, S)$$$

Lean4

instance [Nontrivial R] [IsDomain S] : MulRingNormClass (AbsoluteValue R S) R S :=
  { AbsoluteValue.subadditiveHomClass,
    AbsoluteValue.monoidWithZeroHomClass with
    map_neg_eq_map := fun f => f.map_neg
    eq_zero_of_map_eq_zero := fun f _ => f.eq_zero.1 }

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