toNonUnitalSubsemiring_strictMono

English

The forgetful map from NonUnitalSubring R to AddSubgroup R is injective: two subrings with same additive subgroup are equal.

Русский

Отображение, забывающее умножение, из NonUnitalSubring R в AddSubgroup R инъективно: подполья с одинаковой аддитивной подгруппой равны.

LaTeX

$$Injective (toAddSubgroup : NonUnitalSubring R → AddSubgroup R)$$

Lean4

@[mono]
theorem toNonUnitalSubsemiring_strictMono :
    StrictMono (toNonUnitalSubsemiring : NonUnitalSubring R → NonUnitalSubsemiring R) := fun _ _ => id

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