An explicit Cauchy family in characteristic zero

The natural nodes 0, ..., N-1 and N, ..., 2N-1 are distinct in every characteristic-zero field. Their Cauchy matrix is therefore totally regular. The same rational entries give the family over the rationals, reals, and complexes.

def Algebraic.Cutwidth.MultiOutput.cauchyCharZero (F : Type u_1) [Field F] (N : ℕ) : Matrix (Fin N) (Fin N) F

The rational-node Cauchy family, interpreted in any field.

Equations

• Algebraic.Cutwidth.MultiOutput.cauchyCharZero F N = Algebraic.Cutwidth.MultiOutput.cauchy (fun (i : Fin N) => ↑↑i) fun (j : Fin N) => ↑(N + ↑j)

theorem Algebraic.Cutwidth.MultiOutput.cauchyCharZero_apply (F : Type u_1) [Field F] (N : ℕ) (i j : Fin N) : cauchyCharZero F N i j = (↑↑i - ↑(N + ↑j))⁻¹

Each coefficient is the reciprocal of the indicated nonzero integer difference.

theorem Algebraic.Cutwidth.MultiOutput.totallyRegular_cauchyCharZero (F : Type u_1) [Field F] [CharZero F] (N : ℕ) : TotallyRegular (cauchyCharZero F N)

All square minors of the natural-node Cauchy family are nonsingular.

theorem Algebraic.Cutwidth.MultiOutput.cauchyCharZero_eq_map_rat (F : Type u_1) [Field F] [CharZero F] (N : ℕ) : cauchyCharZero F N = (cauchyCharZero ℚ N).map ⇑(Rat.castHom F)

The entries in every characteristic-zero field are the same explicit rational numbers.