toSubring_subtype — Mathlib

English

Equality of subring subtype and star-subalgebra subtype.

Русский

Равенство подтипов подкольца и звездной подпалгебры.

LaTeX

$$toSubring_subtype : NonUnitalSubringClass.subtype S = NonUnitalStarSubalgebraClass.subtype S$$

Lean4

@[simp]
theorem toSubring_subtype {R A : Type*} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [Star A]
    (S : NonUnitalStarSubalgebra R A) : NonUnitalSubringClass.subtype S = NonUnitalStarSubalgebraClass.subtype S :=
  rfl

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