isStarNormal_add — 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)) \wedge IsStarNormal(a) \wedge IsStarNormal(b) \Rightarrow IsStarNormal(a+b)$$$

Lean4

theorem isStarNormal_add [NonUnitalNonAssocSemiring R] [StarRing R] {a b : R} (hab : Commute a (star b))
    [ha : IsStarNormal a] [hb : IsStarNormal b] : IsStarNormal (a + b) :=
  by
  rw [isStarNormal_iff] at ha hb ⊢
  have := _root_.star_star b ▸ hab.star_star
  simp only [star_add, commute_iff_eq, mul_add, add_mul]
  rw [ha.eq, hb.eq, add_add_add_comm, hab.eq, this.eq]

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