Source / pinned edition
mathlib.divisibility
Source of package mathlib.divisibility · sha256:ee960c38fa27843a12c9542941d5eccb42b42f00199da6af89ee17cbf5bee54c
- work
- urn:arxo:mathlib.divisibility#Import_Source_b0633945066967f025793780617bc4bf036f0f076b498290a1db92acdb2b0f90
- number
- sha256:ee960c38fa27843a12c9542941d5eccb42b42f00199da6af89ee17cbf5bee54c
- kind
- urn:arxo:mathlib.divisibility#treatise
Import_Edition_b0633945066967f025793780617bc4bf036f0f076b498290a1db92acdb2b0f90
- edition
- urn:arxo:mathlib.divisibility#Import_Edition_b0633945066967f025793780617bc4bf036f0f076b498290a1db92acdb2b0f90
- 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/Group/Defs.lean | text/plain; charset=utf-8 | sha256:15119bf00cbb5e31beee450c4ee72967250387fd1532652041c971b304753def | 2026-09-07T23:26:52Z |
Fragments — 1
Monoid.toSemigroup · defn · referenced by: 1
en · official · sha256:c27c0216b33914bb8f078047b56933a8b8231157417fc07176b0e606893b9466
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; rflReferencing norms: Import_Rule_42112ffce927955a7fd6a1a248e9c9ea209b4adae21d6e2a096c86c1c902943c
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.