diff --git a/docs/user/src/lean/basics/factorial.lean b/docs/user/src/lean/basics/factorial.lean
new file mode 100644
index 000000000..86e31fbaa
--- /dev/null
+++ b/docs/user/src/lean/basics/factorial.lean
@@ -0,0 +1,26 @@
+import Base
+
+/-!
+
+# Computing factorial
+
+-/
+
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace factorial
+
+/- [factorial::factorial]:
+   Source: 'src/factorial.rs', lines 1:0-1:27 -/
+divergent def factorial (n : U64) : Result U64 :=
+  if n = 0#u64
+  then Result.ok 1#u64
+  else do
+       let i ← n - 1#u64
+       let i1 ← factorial i
+       n * i1
+
+end factorial
diff --git a/docs/user/src/lean/basics/factorial.lean.md b/docs/user/src/lean/basics/factorial.lean.md
new file mode 100644
index 000000000..8a91f2f2d
--- /dev/null
+++ b/docs/user/src/lean/basics/factorial.lean.md
@@ -0,0 +1 @@
+{{#include factorial.lean}}