AMS Subject classification

This file defines some tools used by the ProblemSubject attribute in order classify problems by their corresponding AMS Subject.

The AMSDescription has one term for each number n ∈ {1, ..., 96} that has a corresponding AMS subject, namely AMSDescription.«n». Note that not all values of n in this interval are assigned a subject.

To extract the value corresponding to n, one can use numToAMSDescriptions n. This is useful for getting the doctring that corresponds to the subject n when parsing the attribute.

Finally, to access the list of subjects and their corresponding number when editing Lean files, we implement a #AMS command that prints this list.

inductive AMS : Type

• «0» : AMS

  General and overarching topics

• «1» : AMS

  History and biography

• «3» : AMS

  Mathematical logic and foundations

• «5» : AMS

  Combinatorics

• «6» : AMS

  Order, lattices, ordered algebraic structures

• «8» : AMS

  General algebraic systems

• «11» : AMS

  Number theory

• «12» : AMS

  Field theory and polynomials

• «13» : AMS

  Commutative algebra

• «14» : AMS

  Algebraic geometry

• «15» : AMS

  Linear and multilinear algebra; matrix theory

• «16» : AMS

  Associative rings and algebras

• «17» : AMS

  Nonassociative rings and algebras

• «18» : AMS

  Category theory; homological algebra

• «19» : AMS

  K-theory

• «20» : AMS

  Group theory and generalizations

• «22» : AMS

  Topological groups, Lie groups

• «26» : AMS

  Real functions

• «28» : AMS

  Measure and integration

• «30» : AMS

  Functions of a complex variable

• «31» : AMS

  Potential theory

• «32» : AMS

  Several complex variables and analytic spaces

• «33» : AMS

  Special functions

• «34» : AMS

  Ordinary differential equations

• «35» : AMS

  Partial differential equations

• «37» : AMS

  Dynamical systems and ergodic theory

• «39» : AMS

  Difference and functional equations

• «40» : AMS

  Sequences, series, summability

• «41» : AMS

  Approximations and expansions

• «42» : AMS

  Harmonic analysis on Euclidean spaces

• «43» : AMS

  Abstract harmonic analysis

• «44» : AMS

  Integral transforms, operational calculus

• «45» : AMS

  Integral equations

• «46» : AMS

  Functional analysis

• «47» : AMS

  Operator theory

• «49» : AMS

  Calculus of variations and optimal control; optimization

• «51» : AMS

  Geometry

• «52» : AMS

  Convex and discrete geometry

• «53» : AMS

  Differential geometry

• «54» : AMS

  General topology

• «55» : AMS

  Algebraic topology

• «57» : AMS

  Manifolds and cell complexes

• «58» : AMS

  Global analysis, analysis on manifolds

• «60» : AMS

  Probability theory and stochastic processes

• «62» : AMS

  Statistics

• «65» : AMS

  Numerical analysis

• «68» : AMS

  Computer science

• «70» : AMS

  Mechanics of particles and systems

• «74» : AMS

  Mechanics of deformable solids

• «76» : AMS

  Fluid mechanics

• «78» : AMS

  Optics, electromagnetic theory

• «80» : AMS

  Classical thermodynamics, heat transfer

• «81» : AMS

  Quantum theory

• «82» : AMS

  Statistical mechanics, structure of matter

• «83» : AMS

  Relativity and gravitational theory

• «85» : AMS

  Astronomy and astrophysics

• «86» : AMS

  Geophysics

• «90» : AMS

  Operations research, mathematical programming

• «91» : AMS

  Game theory, economics, social and behavioral sciences

• «92» : AMS

  Biology and other natural sciences

• «93» : AMS

  Systems theory; control

• «94» : AMS

  Information and communication, circuits

• «97» : AMS

  Mathematics education

def instInhabitedAMS.default : AMS

Equations

• instInhabitedAMS.default = AMS.«0»

instance instInhabitedAMS : Inhabited AMS

Equations

• instInhabitedAMS = { default := instInhabitedAMS.default }

def instBEqAMS.beq : AMS → AMS → Bool

Equations

• instBEqAMS.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instBEqAMS : BEq AMS

Equations

• instBEqAMS = { beq := instBEqAMS.beq }

def instHashableAMS.hash : AMS → UInt64

Equations

• instHashableAMS.hash AMS.«0» = 0
• instHashableAMS.hash AMS.«1» = 1
• instHashableAMS.hash AMS.«3» = 2
• instHashableAMS.hash AMS.«5» = 3
• instHashableAMS.hash AMS.«6» = 4
• instHashableAMS.hash AMS.«8» = 5
• instHashableAMS.hash AMS.«11» = 6
• instHashableAMS.hash AMS.«12» = 7
• instHashableAMS.hash AMS.«13» = 8
• instHashableAMS.hash AMS.«14» = 9
• instHashableAMS.hash AMS.«15» = 10
• instHashableAMS.hash AMS.«16» = 11
• instHashableAMS.hash AMS.«17» = 12
• instHashableAMS.hash AMS.«18» = 13
• instHashableAMS.hash AMS.«19» = 14
• instHashableAMS.hash AMS.«20» = 15
• instHashableAMS.hash AMS.«22» = 16
• instHashableAMS.hash AMS.«26» = 17
• instHashableAMS.hash AMS.«28» = 18
• instHashableAMS.hash AMS.«30» = 19
• instHashableAMS.hash AMS.«31» = 20
• instHashableAMS.hash AMS.«32» = 21
• instHashableAMS.hash AMS.«33» = 22
• instHashableAMS.hash AMS.«34» = 23
• instHashableAMS.hash AMS.«35» = 24
• instHashableAMS.hash AMS.«37» = 25
• instHashableAMS.hash AMS.«39» = 26
• instHashableAMS.hash AMS.«40» = 27
• instHashableAMS.hash AMS.«41» = 28
• instHashableAMS.hash AMS.«42» = 29
• instHashableAMS.hash AMS.«43» = 30
• instHashableAMS.hash AMS.«44» = 31
• instHashableAMS.hash AMS.«45» = 32
• instHashableAMS.hash AMS.«46» = 33
• instHashableAMS.hash AMS.«47» = 34
• instHashableAMS.hash AMS.«49» = 35
• instHashableAMS.hash AMS.«51» = 36
• instHashableAMS.hash AMS.«52» = 37
• instHashableAMS.hash AMS.«53» = 38
• instHashableAMS.hash AMS.«54» = 39
• instHashableAMS.hash AMS.«55» = 40
• instHashableAMS.hash AMS.«57» = 41
• instHashableAMS.hash AMS.«58» = 42
• instHashableAMS.hash AMS.«60» = 43
• instHashableAMS.hash AMS.«62» = 44
• instHashableAMS.hash AMS.«65» = 45
• instHashableAMS.hash AMS.«68» = 46
• instHashableAMS.hash AMS.«70» = 47
• instHashableAMS.hash AMS.«74» = 48
• instHashableAMS.hash AMS.«76» = 49
• instHashableAMS.hash AMS.«78» = 50
• instHashableAMS.hash AMS.«80» = 51
• instHashableAMS.hash AMS.«81» = 52
• instHashableAMS.hash AMS.«82» = 53
• instHashableAMS.hash AMS.«83» = 54
• instHashableAMS.hash AMS.«85» = 55
• instHashableAMS.hash AMS.«86» = 56
• instHashableAMS.hash AMS.«90» = 57
• instHashableAMS.hash AMS.«91» = 58
• instHashableAMS.hash AMS.«92» = 59
• instHashableAMS.hash AMS.«93» = 60
• instHashableAMS.hash AMS.«94» = 61
• instHashableAMS.hash AMS.«97» = 62

instance instHashableAMS : Hashable AMS

Equations

• instHashableAMS = { hash := instHashableAMS.hash }

def instToExprAMS.toExpr : AMS → Lean.Expr

Equations

• instToExprAMS.toExpr AMS.«0» = Lean.Expr.const `AMS.«0» []
• instToExprAMS.toExpr AMS.«1» = Lean.Expr.const `AMS.«1» []
• instToExprAMS.toExpr AMS.«3» = Lean.Expr.const `AMS.«3» []
• instToExprAMS.toExpr AMS.«5» = Lean.Expr.const `AMS.«5» []
• instToExprAMS.toExpr AMS.«6» = Lean.Expr.const `AMS.«6» []
• instToExprAMS.toExpr AMS.«8» = Lean.Expr.const `AMS.«8» []
• instToExprAMS.toExpr AMS.«11» = Lean.Expr.const `AMS.«11» []
• instToExprAMS.toExpr AMS.«12» = Lean.Expr.const `AMS.«12» []
• instToExprAMS.toExpr AMS.«13» = Lean.Expr.const `AMS.«13» []
• instToExprAMS.toExpr AMS.«14» = Lean.Expr.const `AMS.«14» []
• instToExprAMS.toExpr AMS.«15» = Lean.Expr.const `AMS.«15» []
• instToExprAMS.toExpr AMS.«16» = Lean.Expr.const `AMS.«16» []
• instToExprAMS.toExpr AMS.«17» = Lean.Expr.const `AMS.«17» []
• instToExprAMS.toExpr AMS.«18» = Lean.Expr.const `AMS.«18» []
• instToExprAMS.toExpr AMS.«19» = Lean.Expr.const `AMS.«19» []
• instToExprAMS.toExpr AMS.«20» = Lean.Expr.const `AMS.«20» []
• instToExprAMS.toExpr AMS.«22» = Lean.Expr.const `AMS.«22» []
• instToExprAMS.toExpr AMS.«26» = Lean.Expr.const `AMS.«26» []
• instToExprAMS.toExpr AMS.«28» = Lean.Expr.const `AMS.«28» []
• instToExprAMS.toExpr AMS.«30» = Lean.Expr.const `AMS.«30» []
• instToExprAMS.toExpr AMS.«31» = Lean.Expr.const `AMS.«31» []
• instToExprAMS.toExpr AMS.«32» = Lean.Expr.const `AMS.«32» []
• instToExprAMS.toExpr AMS.«33» = Lean.Expr.const `AMS.«33» []
• instToExprAMS.toExpr AMS.«34» = Lean.Expr.const `AMS.«34» []
• instToExprAMS.toExpr AMS.«35» = Lean.Expr.const `AMS.«35» []
• instToExprAMS.toExpr AMS.«37» = Lean.Expr.const `AMS.«37» []
• instToExprAMS.toExpr AMS.«39» = Lean.Expr.const `AMS.«39» []
• instToExprAMS.toExpr AMS.«40» = Lean.Expr.const `AMS.«40» []
• instToExprAMS.toExpr AMS.«41» = Lean.Expr.const `AMS.«41» []
• instToExprAMS.toExpr AMS.«42» = Lean.Expr.const `AMS.«42» []
• instToExprAMS.toExpr AMS.«43» = Lean.Expr.const `AMS.«43» []
• instToExprAMS.toExpr AMS.«44» = Lean.Expr.const `AMS.«44» []
• instToExprAMS.toExpr AMS.«45» = Lean.Expr.const `AMS.«45» []
• instToExprAMS.toExpr AMS.«46» = Lean.Expr.const `AMS.«46» []
• instToExprAMS.toExpr AMS.«47» = Lean.Expr.const `AMS.«47» []
• instToExprAMS.toExpr AMS.«49» = Lean.Expr.const `AMS.«49» []
• instToExprAMS.toExpr AMS.«51» = Lean.Expr.const `AMS.«51» []
• instToExprAMS.toExpr AMS.«52» = Lean.Expr.const `AMS.«52» []
• instToExprAMS.toExpr AMS.«53» = Lean.Expr.const `AMS.«53» []
• instToExprAMS.toExpr AMS.«54» = Lean.Expr.const `AMS.«54» []
• instToExprAMS.toExpr AMS.«55» = Lean.Expr.const `AMS.«55» []
• instToExprAMS.toExpr AMS.«57» = Lean.Expr.const `AMS.«57» []
• instToExprAMS.toExpr AMS.«58» = Lean.Expr.const `AMS.«58» []
• instToExprAMS.toExpr AMS.«60» = Lean.Expr.const `AMS.«60» []
• instToExprAMS.toExpr AMS.«62» = Lean.Expr.const `AMS.«62» []
• instToExprAMS.toExpr AMS.«65» = Lean.Expr.const `AMS.«65» []
• instToExprAMS.toExpr AMS.«68» = Lean.Expr.const `AMS.«68» []
• instToExprAMS.toExpr AMS.«70» = Lean.Expr.const `AMS.«70» []
• instToExprAMS.toExpr AMS.«74» = Lean.Expr.const `AMS.«74» []
• instToExprAMS.toExpr AMS.«76» = Lean.Expr.const `AMS.«76» []
• instToExprAMS.toExpr AMS.«78» = Lean.Expr.const `AMS.«78» []
• instToExprAMS.toExpr AMS.«80» = Lean.Expr.const `AMS.«80» []
• instToExprAMS.toExpr AMS.«81» = Lean.Expr.const `AMS.«81» []
• instToExprAMS.toExpr AMS.«82» = Lean.Expr.const `AMS.«82» []
• instToExprAMS.toExpr AMS.«83» = Lean.Expr.const `AMS.«83» []
• instToExprAMS.toExpr AMS.«85» = Lean.Expr.const `AMS.«85» []
• instToExprAMS.toExpr AMS.«86» = Lean.Expr.const `AMS.«86» []
• instToExprAMS.toExpr AMS.«90» = Lean.Expr.const `AMS.«90» []
• instToExprAMS.toExpr AMS.«91» = Lean.Expr.const `AMS.«91» []
• instToExprAMS.toExpr AMS.«92» = Lean.Expr.const `AMS.«92» []
• instToExprAMS.toExpr AMS.«93» = Lean.Expr.const `AMS.«93» []
• instToExprAMS.toExpr AMS.«94» = Lean.Expr.const `AMS.«94» []
• instToExprAMS.toExpr AMS.«97» = Lean.Expr.const `AMS.«97» []

instance instToExprAMS : Lean.ToExpr AMS

Equations

• instToExprAMS = { toExpr := instToExprAMS.toExpr, toTypeExpr := Lean.Expr.const `AMS [] }

def numToAMSName (n : Nat) : Lean.MetaM Lean.Name

Equations

• One or more equations did not get rendered due to their size.

def AMS.getDesc (a : AMS) : Lean.CoreM String

Equations

• One or more equations did not get rendered due to their size.

def AMS.toNat? (a : AMS) : Option Nat

Equations

• a.toNat? = match Lean.toExpr a with | Lean.Expr.const (pre.str m) [] => m.toNat? | x => none

unsafe def numToAMSSubjects (n : Nat) : Lean.MetaM AMS

Equations

• numToAMSSubjects n = do let nm ← numToAMSName n Lean.Meta.evalExpr AMS q(AMS) (Lean.Expr.const nm [])

def «command#AMS» : Lean.ParserDescr

The #AMS outputs a list of the AMS Math Subjects and their correponding indices

Equations

• «command#AMS» = Lean.ParserDescr.node `«command#AMS» 1024 (Lean.ParserDescr.symbol "#AMS")