The pigeonhole step, stated independently of Latin squares.

theorem LatinQuarter.product_eq_zero_of_repeated_square_zero {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] (f : ι → R) {a b : ι} (hab : a ≠ b) (heq : f a = f b) (hsq : f a * f a = 0) : ∏ i : ι, f i = 0

theorem LatinQuarter.product_eq_zero_of_card_lt {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] (z : κ → R) (hz : ∀ (j : κ), z j * z j = 0) (f : ι → κ) (hcard : Fintype.card κ < Fintype.card ι) : ∏ i : ι, z (f i) = 0

theorem LatinQuarter.span_square_zero_pow_eq_bot {R : Type u_1} [CommRing R] {κ : Type u_2} [Fintype κ] (z : κ → R) (hz : ∀ (j : κ), z j * z j = 0) {d : ℕ} (hd : Fintype.card κ < d) : Ideal.span (Set.range z) ^ d = ⊥