Lean 4 på svenska

Grundläggande formalisering med rena omskrivningar utan s.k. tactics

import Mathlib

example (n : ℕ) : Nat.factorial (n + 1) - (Nat.factorial n) = n * (Nat.factorial n) := by
  rw [Nat.factorial_succ]
  rw [add_mul]
  rw [one_mul]
  rw [add_tsub_cancel_right]

Grundläggande formalisering med tactics

import Mathlib

example (n : ℕ) : Nat.factorial (n + 1) - (Nat.factorial n) = n * (Nat.factorial n) := by
  rw [Nat.factorial_succ]
  ring_nf
  simp

Formalisering där notation för fakultet används (n!)

import Mathlib

open scoped Nat

example (n : ℕ) : (n + 1)! - (n !) = n * (n !) := by
  rw [Nat.factorial_succ]
  ring_nf
  simp

Formalisering där identiteten anpassats för att inte förvirra Leans tactics (genom att undvika subtraktion av naturliga tal)

import Mathlib

open scoped Nat
example (n : ℕ) : (n + 1)! = n * (n !) + (n !) := by
  rw [Nat.factorial_succ]
  ring