toNonUnitalSubsemiring_inj — Mathlib

English

Let S,U be NonUnitalSubalgebras of A. Then S.toNonUnitalSubsemiring = U.toNonUnitalSubsemiring if and only if S = U.

Русский

Пусть S, U — ненулевые подпола A. Тогда S.toNonUnitalSubsemiring = U.toNonUnitalSubsemiring тогда и только тогда, когда S = U.

LaTeX

$$$\forall S,U \in \text{NonUnitalSubalgebra}(R,A),\; S.toNonUnitalSubsemiring = U.toNonUnitalSubsemiring \iff S = U$$$

Lean4

theorem toNonUnitalSubsemiring_inj {S U : NonUnitalSubalgebra R A} :
    S.toNonUnitalSubsemiring = U.toNonUnitalSubsemiring ↔ S = U :=
  toNonUnitalSubsemiring_injective.eq_iff

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