Documentation

Mathlib.Algebra.Star.Orthogonal

Star-orthogonality #

This file develops the basic API for IsStarOrtho, the predicate that two elements p and q of a ⋆-ring are star-orthogonal, i.e., p * star q = 0 and star q * p = 0. This is denoted p ⋆⟂ q with the notation available in the StarRing namespace. The definition is in Mathlib/Algebra/Star/Basic.lean.

Main declarations #

IsSelfAdjoint.isStarOrtho_iff_mul_eq_zero: self-adjoint elements are star-orthogonal if and only if their product is zero.
IsStarOrtho.star_add_mul_add: if p ⋆⟂ q, then star (p + q) * (p + q) = star p * p + star q * q.
IsStarProjection.add_iff_isStarOrtho: the sum of star projections is a star projection if and only if they are star-orthogonal.
IsStarProjection.sum: a finite sum of pairwise star-orthogonal star projections is a star projection.

theorem IsStarOrtho.commute_star {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

Commute p (star q)

theorem IsStarOrtho.star_commute {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

Commute (star p) q

@[simp]

theorem IsStarOrtho.zero_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] (q : R) :

IsStarOrtho 0 q

@[simp]

theorem IsStarOrtho.zero_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] (p : R) :

IsStarOrtho p 0

theorem IsStarOrtho.star {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

IsStarOrtho (star p) (star q)

@[simp]

theorem IsStarOrtho.star_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} :

IsStarOrtho (star p) (star q) ↔ IsStarOrtho p q

theorem IsStarOrtho.op {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

IsStarOrtho (MulOpposite.op p) (MulOpposite.op q)

theorem IsStarOrtho.unop {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : Rᵐᵒᵖ} (h : IsStarOrtho p q) :

IsStarOrtho (MulOpposite.unop p) (MulOpposite.unop q)

@[simp]

theorem IsStarOrtho.op_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} :

IsStarOrtho (MulOpposite.op p) (MulOpposite.op q) ↔ IsStarOrtho p q

@[simp]

theorem IsStarOrtho.unop_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : Rᵐᵒᵖ} :

IsStarOrtho (MulOpposite.unop p) (MulOpposite.unop q) ↔ IsStarOrtho p q

theorem IsStarOrtho.add_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {q p₁ p₂ : R} (h₁ : IsStarOrtho p₁ q) (h₂ : IsStarOrtho p₂ q) :

IsStarOrtho (p₁ + p₂) q

theorem IsStarOrtho.add_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q₁ q₂ : R} (h₁ : IsStarOrtho p q₁) (h₂ : IsStarOrtho p q₂) :

IsStarOrtho p (q₁ + q₂)

theorem IsStarOrtho.smul_left' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} {S : Type u_2} [Star S] [SMulZeroClass S R] [IsScalarTower S R R] [StarModule S R] (h : IsStarOrtho p q) (c : S) :

IsStarOrtho (c • p) q

theorem IsStarOrtho.smul_right' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} {S : Type u_2} [Star S] [SMulZeroClass S R] [IsScalarTower S R R] [StarModule S R] (h : IsStarOrtho p q) (c : S) :

IsStarOrtho p (c • q)

theorem IsStarOrtho.smul_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} {S : Type u_2} [SMulZeroClass S R] [IsScalarTower S R R] [SMulCommClass S R R] (h : IsStarOrtho p q) (c : S) :

IsStarOrtho (c • p) q

theorem IsStarOrtho.smul_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} {S : Type u_2} [SMulZeroClass S R] [IsScalarTower S R R] [SMulCommClass S R R] (h : IsStarOrtho p q) (c : S) :

IsStarOrtho p (c • q)

theorem IsStarOrtho.list_sum_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {q : R} {l : List R} (h : ∀ x ∈ l, IsStarOrtho x q) :

IsStarOrtho l.sum q

theorem IsStarOrtho.list_sum_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p : R} {l : List R} (h : ∀ x ∈ l, IsStarOrtho p x) :

IsStarOrtho p l.sum

theorem IsStarOrtho.multiset_sum_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {q : R} {s : Multiset R} (h : ∀ x ∈ s, IsStarOrtho x q) :

IsStarOrtho s.sum q

theorem IsStarOrtho.multiset_sum_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p : R} {s : Multiset R} (h : ∀ x ∈ s, IsStarOrtho p x) :

IsStarOrtho p s.sum

theorem IsStarOrtho.sum_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {q : R} {ι : Type u_2} {s : Finset ι} {f : ι → R} (h : ∀ i ∈ s, IsStarOrtho (f i) q) :

IsStarOrtho (∑ i ∈ s, f i) q

theorem IsStarOrtho.sum_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p : R} {ι : Type u_2} {s : Finset ι} {f : ι → R} (h : ∀ i ∈ s, IsStarOrtho p (f i)) :

IsStarOrtho p (∑ i ∈ s, f i)

Multiplication #

The properties of star-orthogonality involving multiplication below could be proven manually, and sometimes with weaker hypotheses, but these are provided for convenience because they come up in practice.

theorem IsStarOrtho.mul_left' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p₁ p₂ q : R} (h₁ : star q * p₁ = 0) (h₂ : p₂ * star q = 0) :

IsStarOrtho (p₁ * p₂) q

A version of IsStarOrtho.mul_left with slightly weaker hypotheses.

theorem IsStarOrtho.mul_left {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p₁ p₂ q : R} (h₁ : IsStarOrtho p₁ q) (h₂ : IsStarOrtho p₂ q) :

IsStarOrtho (p₁ * p₂) q

theorem IsStarOrtho.mul_right' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q₁ q₂ : R} (h₁ : star q₁ * p = 0) (h₂ : p * star q₂ = 0) :

IsStarOrtho p (q₁ * q₂)

A version of IsStarOrtho.mul_right with slightly weaker hypotheses.

theorem IsStarOrtho.mul_right {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q₁ q₂ : R} (h₁ : IsStarOrtho p q₁) (h₂ : IsStarOrtho p q₂) :

IsStarOrtho p (q₁ * q₂)

theorem IsStarOrtho.mul' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p₁ p₂ q₁ q₂ : R} (h₁ : star q₁ * p₁ = 0) (h₂ : p₂ * star q₂ = 0) :

IsStarOrtho (p₁ * p₂) (q₁ * q₂)

A version of IsStarOrtho.mul with slightly weaker hypotheses.

theorem IsStarOrtho.mul {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p₁ p₂ q₁ q₂ : R} (h₁ : IsStarOrtho p₁ q₁) (h₂ : IsStarOrtho p₂ q₂) :

IsStarOrtho (p₁ * p₂) (q₁ * q₂)

theorem IsStarOrtho.mul_mul {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p₁ p₂ q₁ q₂ : R} (h₁ : IsStarOrtho p₁ q₁) (h₂ : IsStarOrtho p₂ q₂) (a b : R) :

IsStarOrtho (p₁ * a * p₂) (q₁ * b * q₂)

theorem IsStarOrtho.star_right_conjugate {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) (a b : R) :

IsStarOrtho (p * a * star p) (q * b * star q)

If p and q are star-orthogonal, then so are p * a * star p and q * b * star q.

theorem IsStarOrtho.star_left_conjugate {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) (a b : R) :

IsStarOrtho (star p * a * p) (star q * b * q)

If p and q are star-orthogonal, then so are star p * a * p and star q * b * q.

theorem IsStarOrtho.mul_star_self {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

IsStarOrtho (p * star p) (q * star q)

theorem IsStarOrtho.star_mul_self {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

IsStarOrtho (star p * p) (star q * q)

theorem IsStarOrtho.map {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} {S : Type u_2} {F : Type u_3} [NonUnitalSemiring S] [StarRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] [StarHomClass F R S] (f : F) (h : IsStarOrtho p q) :

IsStarOrtho (f p) (f q)

theorem IsStarOrtho.map_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} {S : Type u_2} {F : Type u_3} [NonUnitalSemiring S] [StarRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] [StarHomClass F R S] {f : F} (hf : Function.Injective ⇑f) :

IsStarOrtho (f p) (f q) ↔ IsStarOrtho p q

theorem IsStarOrtho.star_add_mul_add {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

star (p + q) * (p + q) = star p * p + star q * q

theorem IsStarOrtho.add_mul_star_add {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) :

(p + q) * star (p + q) = p * star p + q * star q

theorem Set.Pairwise.star_sum_mul_sum_of_isStarOrtho {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {ι : Type u_2} {s : Finset ι} {f : ι → R} (h : (↑s).Pairwise (Function.onFun (fun (x1 x2 : R) => IsStarOrtho x1 x2) f)) :

star (∑ i ∈ s, f i) * ∑ i ∈ s, f i = ∑ i ∈ s, star (f i) * f i

theorem Set.Pairwise.sum_mul_star_sum_of_isStarOrtho {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {ι : Type u_2} {s : Finset ι} {f : ι → R} (h : (↑s).Pairwise (Function.onFun (fun (x1 x2 : R) => IsStarOrtho x1 x2) f)) :

(∑ i ∈ s, f i) * star (∑ i ∈ s, f i) = ∑ i ∈ s, f i * star (f i)

theorem Pairwise.star_sum_mul_sum_of_isStarOrtho {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {ι : Type u_2} [Fintype ι] {f : ι → R} (h : Pairwise (Function.onFun (fun (x1 x2 : R) => IsStarOrtho x1 x2) f)) :

star (∑ i : ι, f i) * ∑ i : ι, f i = ∑ i : ι, star (f i) * f i

theorem Pairwise.sum_mul_star_sum_of_isStarOrtho {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {ι : Type u_2} [Fintype ι] {f : ι → R} (h : Pairwise (Function.onFun (fun (x1 x2 : R) => IsStarOrtho x1 x2) f)) :

(∑ i : ι, f i) * star (∑ i : ι, f i) = ∑ i : ι, f i * star (f i)

theorem IsSelfAdjoint.isStarOrtho_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (hp : IsSelfAdjoint p) :

IsStarOrtho p q ↔ p * q = 0 ∧ q * p = 0

theorem IsSelfAdjoint.isStarOrtho_iff' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (hq : IsSelfAdjoint q) :

IsStarOrtho p q ↔ p * q = 0 ∧ q * p = 0

A version of IsSelfAdjoint.isStarOrtho_iff where the right argument is self-adjoint.

theorem IsSelfAdjoint.isStarOrtho_iff_mul_eq_zero {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (hp : IsSelfAdjoint p) (hq : IsSelfAdjoint q) :

IsStarOrtho p q ↔ p * q = 0

Self-adjoint elements are star-orthogonal if and only if their product is zero.

theorem IsStarOrtho.mul_eq_zero {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) (hq : IsSelfAdjoint q) :

q * p = 0

theorem IsStarOrtho.mul_eq_zero' {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) (hq : IsSelfAdjoint q) :

p * q = 0

theorem IsStarOrtho.isStarProjection_add {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) (hp : IsStarProjection p) (hq : IsStarProjection q) :

IsStarProjection (p + q)

The sum of star-orthogonal star projections is a star projection.

theorem IsStarProjection.add_iff_isStarOrtho {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {p q : R} [IsCancelAdd R] [HasUniqueDiv R] (hp : IsStarProjection p) (hq : IsStarProjection q) :

IsStarProjection (p + q) ↔ IsStarOrtho p q

The sum of star projections is a star projection if and only if they are star-orthogonal.

theorem IsStarProjection.sum {R : Type u_1} [NonUnitalSemiring R] [StarRing R] {ι : Type u_2} {s : Finset ι} {f : ι → R} (hf : ∀ i ∈ s, IsStarProjection (f i)) (h : (↑s).Pairwise (Function.onFun (fun (x1 x2 : R) => IsStarOrtho x1 x2) f)) :

IsStarProjection (∑ i ∈ s, f i)

A finite sum of pairwise star-orthogonal star projections is a star projection. The converse holds in a star-ordered ring with proper star. See isStarProjection_sum_iff. The converse is not an immediate corollary of IsStarProjection.add_iff_isStarOrtho because we are not assuming the intermediate sums (i.e., over a subset of s) are star projections.

@[simp]

theorem IsStarOrtho.neg_left_iff {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho (-p) q ↔ IsStarOrtho p q

@[simp]

theorem IsStarOrtho.neg_right_iff {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho p (-q) ↔ IsStarOrtho p q

theorem IsStarOrtho.of_neg_left {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho (-p) q → IsStarOrtho p q

Alias of the forward direction of IsStarOrtho.neg_left_iff.

theorem IsStarOrtho.neg_left {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho p q → IsStarOrtho (-p) q

Alias of the reverse direction of IsStarOrtho.neg_left_iff.

theorem IsStarOrtho.neg_right {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho p q → IsStarOrtho p (-q)

Alias of the reverse direction of IsStarOrtho.neg_right_iff.

theorem IsStarOrtho.of_neg_right {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q : R} :

IsStarOrtho p (-q) → IsStarOrtho p q

Alias of the forward direction of IsStarOrtho.neg_right_iff.

theorem IsStarOrtho.sub_left {R : Type u_1} [NonUnitalRing R] [StarRing R] {q p₁ p₂ : R} (h₁ : IsStarOrtho p₁ q) (h₂ : IsStarOrtho p₂ q) :

IsStarOrtho (p₁ - p₂) q

theorem IsStarOrtho.sub_right {R : Type u_1} [NonUnitalRing R] [StarRing R] {p q₁ q₂ : R} (h₁ : IsStarOrtho p q₁) (h₂ : IsStarOrtho p q₂) :

IsStarOrtho p (q₁ - q₂)

@[simp]

theorem isStarOrtho_one_left {R : Type u_1} [Semiring R] [StarRing R] {q : R} :

IsStarOrtho 1 q ↔ q = 0

@[simp]

theorem isStarOrtho_one_right {R : Type u_1} [Semiring R] [StarRing R] {p : R} :

IsStarOrtho p 1 ↔ p = 0

@[simp]

theorem isStarOrtho_natCast_left {R : Type u_1} [Semiring R] [StarRing R] {q : R} [IsAddTorsionFree R] (n : ℕ) :

IsStarOrtho (↑n) q ↔ q = 0 ∨ n = 0

@[simp]

theorem isStarOrtho_natCast_right {R : Type u_1} [Semiring R] [StarRing R] {p : R} [IsAddTorsionFree R] (n : ℕ) :

IsStarOrtho p ↑n ↔ p = 0 ∨ n = 0

@[simp]

theorem isStarOrtho_ofNat_left {R : Type u_1} [Semiring R] [StarRing R] {q : R} [IsAddTorsionFree R] (n : ℕ) [n.AtLeastTwo] :

IsStarOrtho (OfNat.ofNat n) q ↔ q = 0

@[simp]

theorem isStarOrtho_ofNat_right {R : Type u_1} [Semiring R] [StarRing R] {p : R} [IsAddTorsionFree R] (n : ℕ) [n.AtLeastTwo] :

IsStarOrtho p (OfNat.ofNat n) ↔ p = 0

theorem IsStarOrtho.pow_left {R : Type u_1} [Semiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) {n : ℕ} (hn : n ≠ 0) :

IsStarOrtho (p ^ n) q

theorem IsStarOrtho.pow_right {R : Type u_1} [Semiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) {n : ℕ} (hn : n ≠ 0) :

IsStarOrtho p (q ^ n)

theorem IsStarOrtho.pow_pow {R : Type u_1} [Semiring R] [StarRing R] {p q : R} (h : IsStarOrtho p q) {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :

IsStarOrtho (p ^ m) (q ^ n)

theorem IsStarProjection.isStarOrtho_one_sub {R : Type u_1} [Ring R] [StarRing R] {p : R} (hp : IsStarProjection p) :

IsStarOrtho p (1 - p)

theorem IsStarProjection.one_sub_isStarOrtho {R : Type u_1} [Ring R] [StarRing R] {p : R} (hp : IsStarProjection p) :

IsStarOrtho (1 - p) p

@[simp]

theorem isStarOrtho_self_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] [IsProperStar R] (p : R) :

IsStarOrtho p p ↔ p = 0

theorem IsStarOrtho.star_left_of_isStarNormal {R : Type u_1} [NonUnitalSemiring R] [StarRing R] [IsProperStar R] {a b : R} (h : IsStarOrtho a b) (ha : IsStarNormal a) :

IsStarOrtho (star a) b

If a is normal and a ⋆⟂ b, then star a ⋆⟂ b.

theorem IsStarOrtho.star_right_of_isStarNormal {R : Type u_1} [NonUnitalSemiring R] [StarRing R] [IsProperStar R] {a b : R} (h : IsStarOrtho a b) (ha : IsStarNormal a) :

IsStarOrtho a (star b)

If a is normal and a ⋆⟂ b, then a ⋆⟂ star b.

theorem IsStarNormal.isStarOrtho_star_left_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] [IsProperStar R] {a b : R} (ha : IsStarNormal a) :

IsStarOrtho (star a) b ↔ IsStarOrtho a b

If a is normal, then star a ⋆⟂ b ↔ a ⋆⟂ b.

theorem IsStarNormal.isStarOrtho_star_right_iff {R : Type u_1} [NonUnitalSemiring R] [StarRing R] [IsProperStar R] {a b : R} (ha : IsStarNormal a) :

IsStarOrtho a (star b) ↔ IsStarOrtho a b

If a is normal, then a ⋆⟂ star b ↔ a ⋆⟂ b.

theorem IsStarNormal.isStarOrtho_iff_mul_eq_zero {R : Type u_1} [NonUnitalSemiring R] [StarRing R] [IsProperStar R] {a b : R} (ha : IsStarNormal a) (hab : Commute a b) :

IsStarOrtho a b ↔ a * b = 0

If a is normal and commutes with b, then a ⋆⟂ b if and only if a * b = 0.

theorem isStarOrtho_star_left_iff {R : Type u_1} [NonUnitalCommSemiring R] [StarRing R] [IsProperStar R] {a b : R} :

IsStarOrtho (star a) b ↔ IsStarOrtho a b

When the ring is commutative, star a ⋆⟂ b ↔ a ⋆⟂ b.

theorem IsStarOrtho.star_left {R : Type u_1} [NonUnitalCommSemiring R] [StarRing R] [IsProperStar R] {a b : R} :

IsStarOrtho a b → IsStarOrtho (star a) b

Alias of the reverse direction of isStarOrtho_star_left_iff.

When the ring is commutative, star a ⋆⟂ b ↔ a ⋆⟂ b.

theorem isStarOrtho_star_right_iff {R : Type u_1} [NonUnitalCommSemiring R] [StarRing R] [IsProperStar R] {a b : R} :

IsStarOrtho a (star b) ↔ IsStarOrtho a b

When the ring is commutative, a ⋆⟂ star b ↔ a ⋆⟂ b.

theorem IsStarOrtho.star_right {R : Type u_1} [NonUnitalCommSemiring R] [StarRing R] [IsProperStar R] {a b : R} :

IsStarOrtho a b → IsStarOrtho a (star b)

Alias of the reverse direction of isStarOrtho_star_right_iff.

When the ring is commutative, a ⋆⟂ star b ↔ a ⋆⟂ b.

@[simp]

theorem isStarOrtho_iff_mul_eq_zero_of_comm {R : Type u_1} [NonUnitalCommSemiring R] [StarRing R] [IsProperStar R] {a b : R} :

IsStarOrtho a b ↔ a * b = 0

When the ring is commutative, a ⋆⟂ b if and only if a * b = 0.

theorem IsStarOrtho.mul_eq_zero_of_comm {R : Type u_1} [NonUnitalCommSemiring R] [StarRing R] [IsProperStar R] {a b : R} :

IsStarOrtho a b → a * b = 0

Alias of the forward direction of isStarOrtho_iff_mul_eq_zero_of_comm.

When the ring is commutative, a ⋆⟂ b if and only if a * b = 0.

theorem IsStarOrtho.of_mul_eq_zero {R : Type u_1} [NonUnitalCommSemiring R] [StarRing R] [IsProperStar R] {a b : R} :

a * b = 0 → IsStarOrtho a b

Alias of the reverse direction of isStarOrtho_iff_mul_eq_zero_of_comm.

When the ring is commutative, a ⋆⟂ b if and only if a * b = 0.