Mathlib v4.30 source proposition Int.ModEq.mul

Identifier: F:ml430-int-modeq-mul-6736aa2e
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The proposition declared as `Int.ModEq.mul` in the pinned Mathlib v4.30 source.

Formal statement

∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a * c ≡ b * d [ZMOD n]

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

14 direct dependencies 2 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.mod_eq_mul_general

Kind: kernel-term
Status: checked

Supports: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a * c ≡ b * d [ZMOD n]

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example int_theorem_inventory -- mod_eq_mul_general 2>/dev/null | /usr/bin/grep -cE '^theorem[[:space:]]+Int\.mod_eq_mul_general[[:space:]]')" -ge 1

Evidence notes

build_int_prelude admits Int.mod_eq_mul_general through the trusted Kernel::add_declaration gate, which re-checks the proof term against the stated type, so producing this row at all is a machine-checked proof. New proof, lane int-dvd-mirrors: int_prelude/dvd_gcd_mirrors.rs. The existing p.mod_eq_mul needs 0 < n (it routes through mod_eq_iff_dvd); this is a genuinely UNCONDITIONAL version, built by swapping that bridge for the already-unconditional modeq_to_dvd/dvd_to_modeq (the same trick modeq.rs already used to make the additive family unconditional), plus one extra step (Int.mul_sub) the multiplicative case needs that the additive case does not: dvd n (c*(b-a)) is rewritten to dvd n (c*b - c*a) before feeding dvd_to_modeq. mod_eq_mul_right_general/mod_eq_mul_left_general (both un-declared private helpers) scale each hypothesis and mod_eq_trans chains the two results. int_theorem_inventory rendered type matches this fact formal.statement (∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a * c ≡ b * d [ZMOD n]). int_theorem_inventory exits non-zero for a name that does not exist, and the grep -c count (tested -ge 1, not piped into grep -q) requires the admitted declaration to actually be printed; the anchor requires the exact name followed by whitespace. Verified both ways: the real name greps to a count -ge 1; grepping a fabricated name (Int.mod_eq_mul_general_bogus_xyz) makes int_theorem_inventory fail closed (exit 1, no Int declaration matches).

footprint-Int.mod_eq_mul_general

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Int prelude's trusted surface is empty

Checker command

cargo run -q -p axeyum-lean-kernel --example prelude_axiom_inventory -- --require-axiom-free integer

Evidence notes

prelude_axiom_inventory --require-axiom-free integer enumerates the built Int environment and exits non-zero unless it admits no Axiom, Opaque or Quotient declaration (measured: integer axiom=0). A theorem cannot depend on a trusted declaration the environment does not contain, so an empty trusted surface bounds every individual theorem's footprint by []. int_prelude_tests::every_int_declaration_is_checked_and_axiom_free and derived_laws_have_no_axiom_footprint (both re-run on every int_prelude:: sweep) additionally confirm this theorem's own Kernel::axiom_footprint directly.

Provenance

{
  "date": "2026-08-29",
  "established_by": "not established in this ledger",
  "source": "statement-only extraction of `Int.ModEq.mul` from Mathlib v4.30.0; no proof value was exposed",
  "prior_art": [
    {
      "who": "the Mathlib contributors",
      "what": "the theorem declaration `Int.ModEq.mul`",
      "where": "mathlib4 commit c5ea00351c28e24afc9f0f84379aa41082b1188f (v4.30.0)",
      "year": 2026,
      "attribution": "the proposition was read from the pinned statement-only inventory; the proof term and tactic trace were not consulted"
    }
  ]
}