Lean 4 på svenska

Talteori

import Mathlib

-- Sats: √2 är ett irrationellt tal.
example : Irrational (√2) := by
  exact irrational_sqrt_two
-- Alternativ formulering:
example : √2 ∉ Set.range ((↑) : ℚ → ℝ) := by
  exact irrational_sqrt_two

Analys

import Mathlib
open Polynomial

-- Sats (algebrans fundamentalsats): Varje
-- icke-konstant polynom med komplexa koefficienter
-- har minst en rot i de komplexa talen.
example {f : ℂ[X]} (hf : 0 < degree f) : 
  ∃ z : ℂ, IsRoot f z := by
  exact Complex.exists_root hf

Gruppteori

import Mathlib

-- Sats (Lagranges sats): Ordningen av en delgrupp H 
-- till en ändlig grupp G delar ordningen av
-- gruppen G.
example [Group G] (H : Subgroup G) :
  Nat.card H ∣ Nat.card G := by
  exact Subgroup.card_subgroup_dvd_card H