theorem Hex.WordMod.toNat_injective {m : UInt64} {ctx : _root_.MontCtx m} {a b : WordMod ctx} (h : a.toNat = b.toNat) : a = b

toNat is injective: the represented residue determines the element. Follows from toNat_mul_word (a.val.toNat = a.toNat * word % m) with no Montgomery round-trip lemma.

theorem Hex.WordMod.eq_iff_toNat {m : UInt64} {ctx : _root_.MontCtx m} {a b : WordMod ctx} : a = b ↔ a.toNat = b.toNat

Two Montgomery residues are equal exactly when their natural representatives agree.

@[simp]

theorem Hex.WordMod.ofNat_toNat {m : UInt64} {ctx : _root_.MontCtx m} (a : WordMod ctx) : ofNat a.toNat = a

Round trip: reducing the represented residue back in is the identity.

@[simp]

theorem Hex.WordMod.sub_self {m : UInt64} {ctx : _root_.MontCtx m} (a : WordMod ctx) : a - a = 0

@[instance_reducible]

instance Hex.WordMod.instSemiring_hexHensel {m : UInt64} {ctx : _root_.MontCtx m} : Lean.Grind.Semiring (WordMod ctx)

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.WordMod.neg_neg' {m : UInt64} {ctx : _root_.MontCtx m} (a : WordMod ctx) : - -a = a

@[instance_reducible]

instance Hex.WordMod.instRing_hexHensel {m : UInt64} {ctx : _root_.MontCtx m} : Lean.Grind.Ring (WordMod ctx)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.WordMod.instCommRing_hexHensel {m : UInt64} {ctx : _root_.MontCtx m} : Lean.Grind.CommRing (WordMod ctx)

Equations

• Hex.WordMod.instCommRing_hexHensel = { toRing := Hex.WordMod.instRing_hexHensel, mul_comm := ⋯ }

theorem Hex.ZPoly.intModNat_cast (z : Int) {M : Nat} (hM : 0 < M) : ↑(intModNat z M) = z % ↑M

intModNat as an Int remainder (public form of the private intModNat_eq_emod).

theorem Hex.ZPoly.intModNat_lt' (z : Int) {M : Nat} (hM : 0 < M) : intModNat z M < M

The natural remainder of an integer lies below every positive modulus.

theorem Hex.ZPoly.intModNat_add (x y : Int) {M : Nat} (hM : 0 < M) : intModNat (x + y) M = (intModNat x M + intModNat y M) % M

intModNat commutes with addition modulo M.

theorem Hex.ZPoly.intModNat_mul (x y : Int) {M : Nat} (hM : 0 < M) : intModNat (x * y) M = intModNat x M * intModNat y M % M

intModNat commutes with multiplication modulo M.

theorem Hex.ZPoly.intModNat_sub (x y : Int) {M : Nat} (hM : 0 < M) : intModNat (x - y) M = (intModNat x M + (M - intModNat y M)) % M

intModNat commutes with the full-range modular subtraction used by WordMod (x + (M - y)), matching WordMod.toNat_sub.