Source / pinned edition
mathlib.divisibility
Source of package mathlib.divisibility · sha256:ee960c38fa27843a12c9542941d5eccb42b42f00199da6af89ee17cbf5bee54c
- work
- urn:arxo:mathlib.divisibility#Import_Source_8bd3a20cc35406ce4a2f5b20a2ac6906fd0ee967c504d2e08751ead4bb5fb908
- number
- sha256:ee960c38fa27843a12c9542941d5eccb42b42f00199da6af89ee17cbf5bee54c
- kind
- urn:arxo:mathlib.divisibility#treatise
Import_Edition_8bd3a20cc35406ce4a2f5b20a2ac6906fd0ee967c504d2e08751ead4bb5fb908
- edition
- urn:arxo:mathlib.divisibility#Import_Edition_8bd3a20cc35406ce4a2f5b20a2ac6906fd0ee967c504d2e08751ead4bb5fb908
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- —
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://github.com/leanprover-community/mathlib4/blob/db584cd6d46c92f209a44c0f1c829460d327499d/Mathlib/Algebra/Divisibility/Basic.lean | text/plain; charset=utf-8 | sha256:dc3e41682b147b1938eda99eb6056605fe59f77de9db713deac694f4f0709100 | 2026-09-07T23:26:52Z |
Fragments — 2
dvd_trans · lemma · referenced by: 1
en · official · sha256:879434af9994c9f5202a3bdbab946be855802d3dc7527fc2e182fc06a4439667
@[trans]
theorem dvd_trans : a ∣ b → b ∣ c → a ∣ c
| ⟨d, h₁⟩, ⟨e, h₂⟩ => ⟨d * e, h₁ ▸ h₂.trans <| mul_assoc a d e⟩Referencing norms: Import_Rule_1150e293da3b4d9ac72b4eff22b380fc3a4dbe25931dba02fe9268e6304b8cd5
dvd_refl · lemma · referenced by: 1
en · official · sha256:20803f47e982cc88dc389f7622374efee66ca0ba25c04136a93370a19f10c5e9
@[refl, simp]
theorem dvd_refl (a : α) : a ∣ a :=
Dvd.intro 1 (mul_one a)Referencing norms: Import_Rule_4de44635ffc1c793d4b53db3328172f4dc8bd353c0fa1c8bba3b5861aff6a1b2
The hash beside the text is the sha256 of its exact bytes. It is the check that the text shown matches the one pinned in the package: a divergence fails the oracle’s static analysis.