toNonUnitalSubsemiring_injective — Mathlib

English

The map toNonUnitalSubsemiring: Subsemiring R → NonUnitalSubsemiring R is injective.

Русский

Отображение toNonUnitalSubsemiring: Subsemiring R → NonUnitalSubsemiring R инъективно.

LaTeX

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

Lean4

theorem toNonUnitalSubsemiring_injective : Function.Injective (toNonUnitalSubsemiring : Subsemiring R → _) :=
  fun S₁ S₂ h => SetLike.ext'_iff.2 (show (S₁.toNonUnitalSubsemiring : Set R) = S₂ from SetLike.ext'_iff.1 h)

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