Documentation

HexModArithMathlib.WordMod

source
def HexModArithMathlib.WordMod.toZMod {m : UInt64} {ctx : MontCtx m} (a : Hex.WordMod ctx) :
ZMod m.toNat

Interpret an executable WordMod residue as a Mathlib ZMod class.

Equations
Instances For
    source
    @[simp]
    theorem HexModArithMathlib.WordMod.val_toZMod {m : UInt64} {ctx : MontCtx m} (a : Hex.WordMod ctx) :
    (toZMod a).val = a.toNat

    The canonical representative of a transferred class is the residue's value.

    source
    theorem HexModArithMathlib.WordMod.toZMod_injective {m : UInt64} {ctx : MontCtx m} :
    Function.Injective toZMod

    toZMod is injective: its ZMod value is the residue, which pins the word.

    source
    @[simp]
    theorem HexModArithMathlib.WordMod.toZMod_zero {m : UInt64} {ctx : MontCtx m} :
    toZMod 0 = 0
    source
    @[simp]
    theorem HexModArithMathlib.WordMod.toZMod_add {m : UInt64} {ctx : MontCtx m} (a b : Hex.WordMod ctx) :
    toZMod (a + b) = toZMod a + toZMod b
    source
    @[simp]
    theorem HexModArithMathlib.WordMod.toZMod_mul {m : UInt64} {ctx : MontCtx m} (a b : Hex.WordMod ctx) :
    toZMod (a * b) = toZMod a * toZMod b
    source
    @[simp]
    theorem HexModArithMathlib.WordMod.toZMod_one {m : UInt64} {ctx : MontCtx m} :
    toZMod 1 = 1
    source
    @[simp]
    theorem HexModArithMathlib.WordMod.toZMod_neg {m : UInt64} {ctx : MontCtx m} (a : Hex.WordMod ctx) :
    toZMod (-a) = -toZMod a
    source
    @[simp]
    theorem HexModArithMathlib.WordMod.toZMod_sub {m : UInt64} {ctx : MontCtx m} (a b : Hex.WordMod ctx) :
    toZMod (a - b) = toZMod a - toZMod b
    source
    @[simp]
    theorem HexModArithMathlib.WordMod.toZMod_natCast {m : UInt64} {ctx : MontCtx m} (n : ℕ) :
    toZMod ↑n = ↑n
    source
    @[simp]
    theorem HexModArithMathlib.WordMod.toZMod_intCast {m : UInt64} {ctx : MontCtx m} (z : ℤ) :
    toZMod ↑z = ↑z
    source
    theorem HexModArithMathlib.WordMod.toZMod_pow {m : UInt64} {ctx : MontCtx m} (a : Hex.WordMod ctx) (n : ℕ) :
    toZMod (a ^ n) = toZMod a ^ n
    source
    @[instance_reducible]
    instance HexModArithMathlib.WordMod.instCommRingWordMod_hexModArithMathlib {m : UInt64} {ctx : MontCtx m} :
    CommRing (Hex.WordMod ctx)

    The executable WordMod residue ring is a Mathlib CommRing, pulled back along the injective toZMod.

    Equations
    source
    def HexModArithMathlib.WordMod.toZModRingHom {m : UInt64} {ctx : MontCtx m} :
    Hex.WordMod ctx →+* ZMod m.toNat

    toZMod packaged as a ring homomorphism.

    Equations
    Instances For
      source
      @[simp]
      theorem HexModArithMathlib.WordMod.toZModRingHom_apply {m : UInt64} {ctx : MontCtx m} (a : Hex.WordMod ctx) :
      toZModRingHom a = toZMod a