Источник / закреплённая редакция
mathlib.divisibility
Источник пакета mathlib.divisibility · sha256:ee960c38fa27843a12c9542941d5eccb42b42f00199da6af89ee17cbf5bee54c
- work
- urn:arxo:mathlib.divisibility#Import_Source_b0633945066967f025793780617bc4bf036f0f076b498290a1db92acdb2b0f90
- номер
- sha256:ee960c38fa27843a12c9542941d5eccb42b42f00199da6af89ee17cbf5bee54c
- вид
- urn:arxo:mathlib.divisibility#treatise
Import_Edition_b0633945066967f025793780617bc4bf036f0f076b498290a1db92acdb2b0f90
- edition
- urn:arxo:mathlib.divisibility#Import_Edition_b0633945066967f025793780617bc4bf036f0f076b498290a1db92acdb2b0f90
- язык
- en
- официальность
- official
- материализация
- PINNED_OFFICIAL_BYTES
- жизненный цикл
- —
Публикации
| URI | Тип | documentHash | Получено |
|---|---|---|---|
| https://github.com/leanprover-community/mathlib4/blob/db584cd6d46c92f209a44c0f1c829460d327499d/Mathlib/Algebra/Group/Defs.lean | text/plain; charset=utf-8 | sha256:15119bf00cbb5e31beee450c4ee72967250387fd1532652041c971b304753def | 2026-09-07T23:26:52Z |
Фрагменты — 1
Monoid.toSemigroup · defn · на него ссылаются: 1
en · official · sha256:c27c0216b33914bb8f078047b56933a8b8231157417fc07176b0e606893b9466EN
class Monoid (M : Type u) extends Semigroup M, MulOneClass M, NPow M where
npow := npowRecAuto
/-- Raising to the power `(0 : ℕ)` gives `1`. -/
protected npow_zero (x : M) : x ^ 0 = 1 := by intros; rfl
/-- Raising to the power `(n + 1 : ℕ)` behaves as expected. -/
protected npow_succ (n : ℕ) (x : M) : x ^ (n + 1) = x ^ n * x := by intros; rflСсылаются нормы: Import_Rule_42112ffce927955a7fd6a1a248e9c9ea209b4adae21d6e2a096c86c1c902943c
Хэш рядом с текстом — sha256 его точных байтов. Он и есть проверка того, что показанный текст совпадает с закреплённым в пакете: расхождение роняет статику оракула.