Applying ZMod.finEquiv

Mathlib defines ZMod.finEquiv : Fin n ≃+* ZMod n for [NeZero n] and states nothing about applying it. This file states the two evaluation rules as @[simp] lemmas, so that an argument indexed by Fin n rewrites into ZMod n arithmetic instead of being unfolded at each use.

Main results

• ZMod.finEquiv_apply: ZMod.finEquiv n j is the natural cast of j.val.
• ZMod.finEquiv_symm_apply_val: it is (ZMod.finEquiv n).symm that produces the canonical Fin n representative of an element of ZMod n, and that representative's coerced natural value is the element's val.
• TauCeti.mulModEquiv: multiplication by d modulo p as a permutation of Fin p, for d coprime to p, with its evaluation rule TauCeti.mulModEquiv_apply_val. These take a modulus rather than a ZMod value, so they are not dot notation on ZMod and live in TauCeti.

@[simp]

theorem ZMod.finEquiv_apply {n : ℕ} [NeZero n] (j : Fin n) : (finEquiv n) j = ↑↑j

Applying ZMod.finEquiv is the natural cast. ZMod.finEquiv n j is the image of j.val under Nat.cast.

Mathlib defines finEquiv and states no evaluation rule for it in either direction, so this is the lemma a Fin n-indexed statement rewrites through to reach ZMod n.

@[simp]

theorem ZMod.finEquiv_symm_apply_val {n : ℕ} [NeZero n] (z : ZMod n) : ↑((finEquiv n).symm z) = z.val

The canonical Fin n representative of z : ZMod n has natural value z.val. The representative is produced by (ZMod.finEquiv n).symm, not by finEquiv itself, which maps the other way. This is the companion of finEquiv_apply, and the form needed to index by Fin n an element obtained by solving in ZMod n.

noncomputable def TauCeti.mulModEquiv (p : ℕ) {d : ℕ} [NeZero p] (hdp : d.Coprime p) : Fin p ≃ Fin p

Multiplication by a unit permutes the residues: for d coprime to p, the map b ↦ d b mod p is a permutation of Fin p. It is multiplication by the unit ZMod.unitOfCoprime d hdp of ZMod p, read through ZMod.finEquiv.

Equations

• TauCeti.mulModEquiv p hdp = (ZMod.finEquiv p).trans (Equiv.trans (ZMod.unitOfCoprime d hdp).mulLeft (ZMod.finEquiv p).symm)

@[simp]

theorem TauCeti.mulModEquiv_apply_val (p : ℕ) {d : ℕ} [NeZero p] (hdp : d.Coprime p) (b : Fin p) : ↑((mulModEquiv p hdp) b) = d * ↑b % p

The value of TauCeti.mulModEquiv: it sends b to the residue d b mod p.