Mathlib v4.30 source proposition Int.dvd_mul

Identifier: F:ml430-int-dvd-mul-3a7b94cd
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

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

Formal statement

∀ {a b c : ℤ}, c ∣ a * b ↔ ∃ c₁ c₂, c₁ ∣ a ∧ c₂ ∣ b ∧ c₁ * c₂ = c

Dependencies

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

18 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.dvd_mul_split

Kind: kernel-term
Status: checked

Supports: ∀ {a b c : ℤ}, c ∣ a * b ↔ ∃ c₁ c₂, c₁ ∣ a ∧ c₂ ∣ b ∧ c₁ * c₂ = c

Checker command

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

Evidence notes

`build_int_prelude` admits `Int.dvd_mul_split` through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type. New proof, lane int-dvd-mul-split: `int_prelude/dvd_mul_split.rs`, wired in via one `declare_dvd_mul_split` call after `gcd_scaled_mirrors::declare_all` (last in the build, since it needs `gcd.rs`, `ring.rs`'s `Int.mul_eq_zero`, and the whole Nat prelude). NOT named `Int.dvd_mul` for the same reason the Nat mirror isn't (Mathlib's literal name space collision class). None of the three blockers the prior lane's handoff (docs/plan/status/343-dvd-mul-split.md) identified turned out to be needed: no general `Int.gcd_mul_right` was built (the real content routes entirely through `natAbs c`/`natAbs a`/`natAbs b` and the already-proved `Nat.gcd_mul_right`, so the sign of `b` never has to be split on or reconstructed), no new Int-level cancellation lemma was built (the one cancellation is at the Nat level, via `Nat.mul_left_cancel_of_pos`), and `g1 != 0` from `c != 0` needed only `Nat.eq_zero_of_gcd_eq_zero_left` plus a local copy of `ring.rs`'s private `nat_abs_zero_implies_int_zero`. Witnesses `c1 := ofNat(Nat.gcd(natAbs c, natAbs a))`, `c2 := w` (from Int-level `dvd_elim` on `gcd_dvd_left`, so genuinely Int-signed, never reconstructed from a Nat witness after the fact -- the sign-ambiguous route the handoff correctly warned off). The `c=0` case is handled by a direct case split on `a=0 ∨ b=0` (`Int.mul_eq_zero`), matching the Nat proof's own corner. Reverse direction is the same uniform four-factor regrouping the Nat proof uses, built from `Int.mul_assoc`/`Int.mul_comm` since no `Int.mul_left_comm` field exists. `int_theorem_inventory`'s rendered type is `(x0:Int)->(x1:Int)->(x2:Int)->Iff (Int.dvd x0 (Int.mul x1 x2)) (Exists x3, Exists x4, And (Int.dvd x3 x1) (And (Int.dvd x4 x2) (Eq (Int.mul x3 x4) x0)))`, matching this fact's `formal.statement` exactly (x0/x1/x2/x3/x4 = c/a/b/c1/c2). `int_theorem_inventory` exits non-zero for a name that does not exist (verified: `dvd_mul_split_bogus_xyz` -> exit 1, `error: no Int declaration matches ...`), and the anchored `grep -cE` (tested `-ge 1` directly, not piped through `grep -q`) requires the exact name preceded by `theorem` and followed by whitespace -- verified both directions with `/usr/bin/grep` explicitly (positive count 1, bogus-name count 0).

footprint-Int.dvd_mul_split

Kind: exhaustive-enumeration
Status: checked

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

Checker command

cargo run -q --release -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`, exit 0; the same run's `axreal: axiom=30` row is the separate, unrelated legacy axiomatized-reals package -- see CLAUDE.md's `AxReal`/`CReal` gotcha). A theorem cannot depend on a trusted declaration the environment does not contain, so an empty trusted surface bounds `Int.dvd_mul_split`'s own footprint by []. `int_prelude_tests::every_int_declaration_is_checked_and_axiom_free` additionally checks this theorem's own `Kernel::axiom_footprint` directly via `derived_laws` (it is listed there), and a dedicated test `dvd_mul_split_applies_at_a_discriminating_negative_and_free_degenerate_instance` applies it at three axes: `Iff.mpr` at a discriminating instance where `c` shares a factor with BOTH `a` and `b` (`c=6,a=4,b=9,c1=2,c2=3`, producing a real proof of `Int.dvd 6 36`), `Iff.mp` at a NEGATIVE divisor (`c=-6,a=4,b=9`, witness `-6`), and `Iff.mp` at the `c=0` degenerate branch with a genuinely FREE `b` (pushed into an explicit `LocalContext` as an axiom-declared variable).

Provenance

{
  "date": "2026-08-29",
  "established_by": "not established in this ledger",
  "source": "statement-only extraction of `Int.dvd_mul` from Mathlib v4.30.0; no proof value was exposed",
  "prior_art": [
    {
      "who": "the Mathlib contributors",
      "what": "the theorem declaration `Int.dvd_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"
    }
  ]
}