toNonUnitalSubsemiring_inj — Mathlib

English

The injection toSemiring is injective, i.e., the induced Semiring structure from a subsemiring is determined by the subsemiring.

Русский

Инъекция toSemiring инъективна: индуцированная структура семиринга определяется подпол semiring.

LaTeX

$$Injective (toSemiring) [contextualized in Subsemiring]$$

Lean4

@[simp]
theorem toNonUnitalSubsemiring_inj {S₁ S₂ : Subsemiring R} :
    S₁.toNonUnitalSubsemiring = S₂.toNonUnitalSubsemiring ↔ S₁ = S₂ :=
  toNonUnitalSubsemiring_injective.eq_iff

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