isStarNormal_sub — Mathlib

English

If a commutes with star(b) and a,b are star-normal, then a - b is star-normal.

Русский

Если a коммутирует с star(b) и a,b звёздно-нормальны, то a - b звёздно-нормален.

LaTeX

$$$\forall a,b\, (Commute\ a\ (star\ b)) \Rightarrow(IsStarNormal(a) \land IsStarNormal(b) \Rightarrow IsStarNormal(a-b))$$$

Lean4

theorem isStarNormal_sub [NonUnitalNonAssocRing R] [StarRing R] {a b : R} (hab : Commute a (star b))
    [ha : IsStarNormal a] [hb : IsStarNormal b] : IsStarNormal (a - b) :=
  sub_eq_add_neg a b ▸ (star_neg b ▸ hab.neg_right).isStarNormal_add

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