toNonUnitalSubring — Mathlib

English

Eq of toNonUnitalSubalgebra implies equality of subalgebras.

Русский

Равенство toNonUnitalSubalgebra означает равенство подалгебр.

LaTeX

$$$S.toNonUnitalSubalgebra = U.toNonUnitalSubalgebra \\Rightarrow S = U$$$

Lean4

/-- A non-unital star subalgebra over a ring is also a `Subring`. -/
def toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] [Star A]
    (S : NonUnitalStarSubalgebra R A) : NonUnitalSubring A
    where
  toNonUnitalSubsemiring := S.toNonUnitalSubsemiring
  neg_mem' := neg_mem (s := S)

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