toNonnegHomClass — Mathlib

English

From Group Seminorm Class, obtain NonnegHomClass.

Русский

Из класса полиноморфизмов группы выводится класс неотрицательных гомоморфизмов.

LaTeX

$$$NonnegHomClass(F, \alpha, \beta)$$$

Lean4

@[to_additive]
instance (priority := 100) toNonnegHomClass [Group α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β]
    [GroupSeminormClass F α β] : NonnegHomClass F α β :=
  { ‹GroupSeminormClass F α β› with
    apply_nonneg := fun f a =>
      (nsmul_nonneg_iff two_ne_zero).1 <|
        by
        rw [two_nsmul, ← map_one_eq_zero f, ← div_self' a]
        exact map_div_le_add _ _ _ }

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