The finite Mahler basis of ZMod N → R

The functions x ↦ C(x.val, i), i < N, on ZMod N with values in a nontrivial commutative ring R are linearly independent (the matrix [C(x, i)]_{x, i < N} is lower unitriangular); over a field they form a basis of ZMod N → K.

Main results

• ConjeturaC.linearIndependent_choose: linear independence over R.
• ConjeturaC.chooseBasis, ConjeturaC.coe_chooseBasis: the basis over a field.
• ConjeturaC.linearIndependent_choose_sq: the case N = p², R = ZMod p.

References

• C. Marín, Reading Iwasawa λ-invariants from Mahler matrices modulo p: programs, data and Lean files, Zenodo (2026), doi:10.5281/zenodo.23085315.

def ConjeturaC.chooseFun (N : ℕ) (R : Type u_1) [CommRing R] (i : Fin N) : ZMod N → R

Binomial functions on ZMod N.

Equations

• ConjeturaC.chooseFun N R i x = ↑(x.val.choose ↑i)

theorem ConjeturaC.linearIndependent_choose (N : ℕ) [NeZero N] (R : Type u_1) [CommRing R] [Nontrivial R] : LinearIndependent R (chooseFun N R)

noncomputable def ConjeturaC.chooseBasis (N : ℕ) [NeZero N] (K : Type u_1) [Field K] : Module.Basis (Fin N) K (ZMod N → K)

Over a field, the binomial functions are a basis of ZMod N → K.

Equations

• ConjeturaC.chooseBasis N K = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

theorem ConjeturaC.coe_chooseBasis (N : ℕ) [NeZero N] (K : Type u_1) [Field K] : ⇑(chooseBasis N K) = chooseFun N K

theorem ConjeturaC.linearIndependent_choose_sq (p : ℕ) [Fact (Nat.Prime p)] : LinearIndependent (ZMod p) fun (i : Fin (p ^ 2)) (x : ZMod (p ^ 2)) => ↑(x.val.choose ↑i)

The case of the paper: N = p², values in ZMod p.