toNonUnitalSubsemiring_injective — Mathlib

English

The forgetful map from NonUnitalSubring R to NonUnitalSubsemiring R is injective: equal images imply equal subrings.

Русский

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

LaTeX

$$Injective (toNonUnitalSubsemiring : NonUnitalSubring R → NonUnitalSubsemiring R)$$

Lean4

theorem toNonUnitalSubsemiring_injective :
    Function.Injective (toNonUnitalSubsemiring : NonUnitalSubring R → NonUnitalSubsemiring R)
  | _r, _s, h => ext (SetLike.ext_iff.mp h :)

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