toNonUnitalSubring_inj — Mathlib

English

Equivalently, S.toNonUnitalSubring = U.toNonUnitalSubring if and only if S = U.

Русский

Эквивалентно: S.toNonUnitalSubring = U.toNonUnitalSubring тогда и только тогда, когда S = U.

LaTeX

$$S.toNonUnitalSubring = U.toNonUnitalSubring \leftrightarrow S = U$$

Lean4

theorem toNonUnitalSubring_inj {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] [Star A]
    {S U : NonUnitalStarSubalgebra R A} : S.toNonUnitalSubring = U.toNonUnitalSubring ↔ S = U :=
  toNonUnitalSubring_injective.eq_iff

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