Источник / закреплённая редакция
mathlib.divisibility
Источник пакета mathlib.divisibility · sha256:ee960c38fa27843a12c9542941d5eccb42b42f00199da6af89ee17cbf5bee54c
- work
- urn:arxo:mathlib.divisibility#Import_Source_8bd3a20cc35406ce4a2f5b20a2ac6906fd0ee967c504d2e08751ead4bb5fb908
- номер
- sha256:ee960c38fa27843a12c9542941d5eccb42b42f00199da6af89ee17cbf5bee54c
- вид
- urn:arxo:mathlib.divisibility#treatise
Import_Edition_8bd3a20cc35406ce4a2f5b20a2ac6906fd0ee967c504d2e08751ead4bb5fb908
- edition
- urn:arxo:mathlib.divisibility#Import_Edition_8bd3a20cc35406ce4a2f5b20a2ac6906fd0ee967c504d2e08751ead4bb5fb908
- язык
- en
- официальность
- official
- материализация
- PINNED_OFFICIAL_BYTES
- жизненный цикл
- —
Публикации
| URI | Тип | documentHash | Получено |
|---|---|---|---|
| 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 |
Фрагменты — 2
dvd_trans · lemma · на него ссылаются: 1
en · official · sha256:879434af9994c9f5202a3bdbab946be855802d3dc7527fc2e182fc06a4439667EN
@[trans]
theorem dvd_trans : a ∣ b → b ∣ c → a ∣ c
| ⟨d, h₁⟩, ⟨e, h₂⟩ => ⟨d * e, h₁ ▸ h₂.trans <| mul_assoc a d e⟩Ссылаются нормы: Import_Rule_1150e293da3b4d9ac72b4eff22b380fc3a4dbe25931dba02fe9268e6304b8cd5
dvd_refl · lemma · на него ссылаются: 1
en · official · sha256:20803f47e982cc88dc389f7622374efee66ca0ba25c04136a93370a19f10c5e9EN
@[refl, simp]
theorem dvd_refl (a : α) : a ∣ a :=
Dvd.intro 1 (mul_one a)Ссылаются нормы: Import_Rule_4de44635ffc1c793d4b53db3328172f4dc8bd353c0fa1c8bba3b5861aff6a1b2
Хэш рядом с текстом — sha256 его точных байтов. Он и есть проверка того, что показанный текст совпадает с закреплённым в пакете: расхождение роняет статику оракула.