instAddSubgroupClass — Mathlib

English

I is an additive subgroup of R; in particular, it contains 0, is closed under addition and under negation.

Русский

I является аддитивной подгруппой R; в частности, 0 ∈ I, и I замкнуто относительно сложения и взятия противоположного.

LaTeX

$$0 ∈ I ∧ ∀ x,y ∈ I, x+y ∈ I ∧ ∀ x ∈ I, -x ∈ I$$

Lean4

instance : AddSubgroupClass (TwoSidedIdeal R) R
    where
  zero_mem := zero_mem
  add_mem := @add_mem _ _
  neg_mem := @neg_mem _ _

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