A Known results in mathlib

A.1 Rings

• Commutative ring with unit CommRing

• Field Field

  • assertion that a ring is a field IsField

• assertion that a ring is an integral domain IsDomain

• assertion that a ring is PID: IsDomain + IsPrincipalIdealRing

• assertion that a ring is UFD: IsDomain + UniqueFactorizationMonoid

• Noetherian ring IsNoetherianRing

  • finitely many minimal prime ideals minimalPrimes.finite_of_isNoetherianRing

  • finitely many minimal prime over-ideals Ideal.finite_minimalPrimes_of_isNoetherianRing

• Artin ring IsArtinianRing

  • it is also Noetherian instIsNoetherianRingOfIsArtinianRing (instance, shouldn’t need to call directly)

• Characteristic of a ring ringChar, exponential characteristic ringExpChar

  • assertion that a ring is of specific characteristic CharZero, CharP, ExpChar

• Krull dimension of a ring ringKrullDim

  • assertion that a ring is of Krull dimension \(\leq n\) Ring.KrullDimLE

  • assertion that a ring is of Krull dimension \(\leq 1\) Ring.DimensionLEOne

• Krull dimension of polynomial rings

  • \(\dim R+1\leq \dim R[X]\leq 2\dim R+1\)

    ringKrullDim_succ_le_ringKrullDim_polynomial, Polynomial.ringKrullDim_le

  • \(\dim R[X]=\dim R+1\) if \(R\) is Noetherian #27542

• Regular local ring #25283 (stall)

A.2 Ideals

• Ideal of a ring Ideal

  • assertion that an ideal is principal Submodule.IsPrincipal

  • assertion that an ideal is a prime ideal Ideal.IsPrime

    • Ideal.Quotient.isDomain_iff_prime

  • assertion that an ideal is a maximal ideal Ideal.IsMaximal

    • Ideal.Quotient.maximal_ideal_iff_isField_quotient

    • Ideal.Quotient.field (instance, shouldn’t need to call directly)

• Height of an ideal Ideal.height, height of a prime ideal Ideal.primeHeight

  • assertion that an ideal is the whole ring or of finite height Ideal.FiniteHeight

• the Type of prime ideals of a ring \({\mathrm{Spec}}(R)\) PrimeSpectrum

• set of minimal primes minimalPrimes, set of minimal prime over-ideals Ideal.minimalPrimes

A.3 Modules

• Support of a module \({\mathrm{Supp}}(M)\) Module.support

• Annihilator of a module \({\mathrm{Ann}}(M)\) Module.annihilator

• \(M^*=\operatorname{Hom}_{\mathbb {Z}}(M,{\mathbb {Q}}/{\mathbb {Z}})\) CharacterModule

• Associated primes of a module \(\operatorname{Ass}(M)\) associatedPrimes

• Finitely generated module Module.Finite

• Free module Module.Free

• Projective module Module.Projective

• Injective module Module.Injective

• Flat module Module.Flat

• Torsion module Module.IsTorsion

• Torsion submodule Submodule.torsion

  • Torsion-free module Submodule.torsion R M = ⊥

• Noetherian module IsNoetherian

• Artin module IsArtinian

• assertion that a module is of finite length IsFiniteLength

  • in the statement of theorems use IsNoetherian + IsArtinian instead

  • if and only if exists composition series isFiniteLength_iff_exists_compositionSeries

  • length of a module \(\ell _A(M)\) Module.length

• composition series CompositionSeries

  • usage:

    ∃ (s : CompositionSeries (Submodule R M)), RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤

A.4 Number theory

• assertion that a field is a number field (i.e. finite extension of \({\mathbb {Q}}\)) NumberField

• ring of integers \({\mathcal{O}}_K\) NumberField.RingOfIntegers

• assertion that a ring is a Dedekind domain IsDedekindDomain

  • unique factorization of ideals Ideal.uniqueFactorizationMonoid (instance, shouldn’t need to call directly)

• fraction ideals FractionalIdeal

  • usage: if \(R\) is a domain, \(K\) is fraction field of \(R\), then the Type of fraction ideals in \(K\) is:

    FractionalIdeal (nonZeroDivisors R) K

  • \(\operatorname{ord}_{\mathfrak {p}}({\mathfrak {a}})\) FractionalIdeal.count

• ideal class group ClassGroup

  • finite NumberField.RingOfIntegers.instFintypeClassGroup (instance, shouldn’t need to call directly)

  • class number NumberField.classNumber

• places of a number field \(K\): AbsoluteValue K ℝ, NumberField.place

  • infinite places NumberField.InfinitePlace

  • real and complex places NumberField.InfinitePlace.IsReal, NumberField.InfinitePlace.IsComplex

  • \(r_1,r_2\) NumberField.InfinitePlace.nrRealPlaces, NumberField.InfinitePlace.nrComplexPlaces

  • \(r_1+r_2-1\) NumberField.Units.rank

  • Dirichlet unit theorem NumberField.Units.rank_modTorsion

• assertion that a field extension is abelian #23669 (currently use IsGalois + IsMulCommutative instead)

• assertion that a field extension is cyclotomic IsCyclotomicExtension

  • cyclotomic field \(K(\mu _n)\) CyclotomicField

• \(p\)-adic cyclotomic character: if \(\mu _{p^\infty }\subset L\) then \(\chi _{\mathrm{cyc}}:{\mathrm{Aut}}(L)\to {\mathbb {Z}}_p^\times \) cyclotomicCharacter