Pivot maps of triangular families

If f (π i) (z j) = 0 for i < j while f (π j) (z j) ≠ 0, then the pivot map π is injective (Function.Injective.of_triangular). This is the distinctness of the pivot rows in a triangular family, as produced by Gaussian elimination.

theorem Function.Injective.of_triangular {ι : Type u_1} {κ : Type u_2} {M : Type u_3} {N : Type u_4} [LinearOrder ι] [Zero N] {f : κ → M → N} {z : ι → M} {π : ι → κ} (h₀ : ∀ (i j : ι), i < j → f (π i) (z j) = 0) (hp : ∀ (j : ι), f (π j) (z j) ≠ 0) : Injective π

The pivot rows of a triangular family are distinct: if f (π i) (z j) = 0 for i < j while f (π j) (z j) ≠ 0, then π is injective.