Vanishing products for three indexed arms #
In an associative non-unital semiring, suppose each d a * u a vanishes and the sum of the
opposite products u a * d a vanishes. When there are at most three indices, every length-five
product through three such arms vanishes. The opposite-ring version gives the reversed product.
A vanishing identity for three arms #
theorem
TauCeti.mul_mul_eq_zero_of_card_le_three
{A : Type u_1}
{L : Type u_2}
[NonUnitalSemiring A]
[Fintype L]
(hL : Fintype.card L ≤ 3)
(u d : L → A)
(hdu : ∀ (a : L), d a * u a = 0)
(hsum : ∑ a : L, u a * d a = 0)
(a b c : L)
:
In a non-unital semiring, let u a and d a be indexed by a type with at most three
elements, with d a * u a = 0 for every a and ∑ a, u a * d a = 0. Then every product
(u a * d a) * (u b * d b) * u c vanishes.
theorem
TauCeti.mul_mul_eq_zero_of_card_le_three'
{A : Type u_1}
{L : Type u_2}
[NonUnitalSemiring A]
[Fintype L]
(hL : Fintype.card L ≤ 3)
(u d : L → A)
(hdu : ∀ (a : L), d a * u a = 0)
(hsum : ∑ a : L, u a * d a = 0)
(a b c : L)
:
The dual form of mul_mul_eq_zero_of_card_le_three, read in the opposite ring: every product
d c * (u b * d b) * (u a * d a) vanishes.