Lean 4 på svenska

Den algebraiska hierarkin från icke-unitära ringar till algebraiska slutna kroppar uttryckt i Lean med hjälp av Mathlib.

import Mathlib
noncomputable section
set_option autoImplicit false
open Polynomial

class IntegralDomain (P : Type*) extends CommRing P, IsDomain P
instance (P : Type*) [CommRing P] [IsDomain P] : IntegralDomain P := {}
class UniqueFactorizationDomain (P : Type*) extends IntegralDomain P, UniqueFactorizationMonoid P
instance (P : Type*) [IntegralDomain P] [UniqueFactorizationMonoid P] : UniqueFactorizationDomain P := {}
class PrincipalIdealDomain (P : Type*) extends UniqueFactorizationDomain P, IsPrincipalIdealRing P
instance (P : Type*) [UniqueFactorizationDomain P] [IsPrincipalIdealRing P] : PrincipalIdealDomain P := {}
class AlgebraicallyClosedField (P : Type*) extends Field P, IsAlgClosed P
instance (P : Type*) [Field P] [IsAlgClosed P] : AlgebraicallyClosedField P := {}

-- En algebraiskt sluten kropp är en kropp <https://sv.wikipedia.org/wiki/Kropp_(algebra)>
example (α : Type) [AlgebraicallyClosedField α] : Field α := by infer_instance
-- En kropp är ett euklidisk område <https://sv.wikipedia.org/wiki/Euklidiskt_omr%C3%A5de>
example (α : Type) [Field α] : EuclideanDomain α := by infer_instance
-- Ett euklidisk område är en principalidealdomän <https://sv.wikipedia.org/wiki/Principalidealdom%C3%A4n>
example (α : Type) [EuclideanDomain α] : PrincipalIdealDomain α := by infer_instance
-- En principalidealdomän är en ring med entydig faktorisering <https://sv.wikipedia.org/wiki/EF-ring>
example (α : Type) [PrincipalIdealDomain α] : UniqueFactorizationDomain α := by infer_instance
-- En ring med entydig faktorisering är ett integritetsområde <https://sv.wikipedia.org/wiki/Integritetsomr%C3%A5de>
example (α : Type) [UniqueFactorizationDomain α] : IntegralDomain α := by infer_instance
-- En integritetsområde är en kommutativ ring <https://sv.wikipedia.org/wiki/Kommutativ_ring>
example (α : Type) [IntegralDomain α] : CommRing α := by infer_instance
-- En kommutativ (unitär) ring är en unitär ring <https://sv.wikipedia.org/wiki/Ring_(matematik)>
example (α : Type) [CommRing α] : Ring α := by infer_instance
-- En unitär ring är en ickeunitär (eller unitär) ring <https://sv.wikipedia.org/wiki/Ring_(matematik)>
example (α : Type) [Ring α] : NonUnitalRing α := by infer_instance

-- Exempel:
--
-- # ICKEUNITÄR RING <https://sv.wikipedia.org/wiki/Ring_(matematik)>
-- De jämna heltalen (2ℤ) utgör en ickeunitär ring (en ring utan etta).
example : NonUnitalRing (TwoSidedIdeal.span {(2 : ℤ)}) := by infer_instance

-- # RING (MED ETTA) <https://sv.wikipedia.org/wiki/Ring_(matematik)>
-- Kvadratiska matriser med med heltalselement utgör en (unitär) ring (en ring med etta).
example (n : ℕ) : Ring (Matrix (Fin n) (Fin n) ℤ) := by infer_instance

-- # KOMMUTATIV RING <https://sv.wikipedia.org/wiki/Kommutativ_ring>
-- ℤ/nℤ utgör en kommutativ ring.
example (n : ℕ) : CommRing (ZMod n) := by infer_instance

-- # INTEGRITETSOMRÅDE <https://sv.wikipedia.org/wiki/Integritetsomr%C3%A5de>
-- Heltalen utgör ett integritetsområde.
--# TODO...
example : IntegralDomain ℤ := by infer_instance

-- # RING MED ENTYDIG FAKTORISERING <https://sv.wikipedia.org/wiki/EF-ring>
-- Polynomringen över heltalen utgör en ring med entydig faktorisering.
example : UniqueFactorizationDomain ℤ[X] := by infer_instance

-- # PRINCIPALIDEALDOMÄN <https://sv.wikipedia.org/wiki/Principalidealdom%C3%A4n>
-- Heltalen utgör en principalidealdomän.
--# TODO...
example : PrincipalIdealDomain ℤ := by infer_instance

-- # EUKLIDISKT OMRÅDE <https://sv.wikipedia.org/wiki/Euklidiskt_omr%C3%A5de>
-- Heltalen utgör en euklidiskt område.
example : EuclideanDomain ℤ := by infer_instance
-- Polynomringen över de reella talen utgör en euklidiskt område.
example : EuclideanDomain ℝ[X] := by infer_instance

-- # KROPP <https://sv.wikipedia.org/wiki/Kropp_(algebra)>
-- De rationella talen utgör en kropp.
example : Field ℚ := by infer_instance
-- De reella talen utgör en kropp.
example : Field ℝ := by infer_instance
-- ℤ/pℤ utgör en kropp.
example (p : ℕ) [h : Fact (Nat.Prime p)] : Field (ZMod p) := by infer_instance

-- # ALGEBRAISKT SLUTEN KROPP <https://sv.wikipedia.org/wiki/Kropp_(algebra)>
-- De komplexa talen utgör en algebraiskt sluten kropp.
example : AlgebraicallyClosedField ℂ := by infer_instance