Dummit and Foote definition catalogue

Title: Abstract Algebra, third edition

Authors: David S. Dummit and Richard M. Foote

Zotero key: A4FFDNKB

Citekey: DF04

Source attachment: local-write-api-1783380265761-A4FFDNKB_extracted.md

Preliminary chapter

• Set — §0.1, Basics, p. 1
  • Mathlib: Set — Mathlib/Data/Set/Defs.lean
• Function — §0.1, Basics, p. 1
  • Mathlib: Function — Mathlib/Logic/Function/Basic.lean
• Equivalence relation — §0.1, Basics, p. 1
  • Mathlib: Equivalence — Mathlib/Logic/Relation.lean
• Partition — §0.1, Basics, p. 1
  • Mathlib: Setoid.IsPartition — Mathlib/Data/Setoid/Partition.lean
• Divisibility — §0.2, Properties of the Integers, p. 4
  • Mathlib: Dvd.dvd — Init/Prelude.lean:1560 (Lean core, not Mathlib)
• Greatest common divisor — §0.2, Properties of the Integers, p. 4
  • Mathlib: gcd — Mathlib/Data/Nat/GCD/Basic.lean
• Congruence modulo n — §0.3, Z/nZ: The Integers Modulo n, p. 8
  • Mathlib: Nat.ModEq — Mathlib/Data/Nat/ModEq.lean
• Residue class — §0.3, Z/nZ: The Integers Modulo n, p. 8
  • Mathlib: ZMod — Mathlib/Data/ZMod/Basic.lean

Chapter 1: Introduction to Groups

• Binary operation — §1.1, Basic Axioms and Examples, p. 16
  • Mathlib: Mul — Mathlib/Algebra/Group/Defs.lean
• Group — §1.1, Basic Axioms and Examples, p. 16
  • Mathlib: Group — Mathlib/Algebra/Group/Defs.lean
• Abelian group — §1.1, Basic Axioms and Examples, p. 16
  • Mathlib: CommGroup — Mathlib/Algebra/Group/Defs.lean
• Order of a group — §1.1, Basic Axioms and Examples, p. 16
  • Mathlib: Nat.card — Mathlib/SetTheory/Cardinal/Finite.lean
• Order of an element — §1.1, Basic Axioms and Examples, p. 16
  • Mathlib: orderOf — Mathlib/GroupTheory/OrderOfElement.lean
• Dihedral group — §1.2, Dihedral Groups, p. 23
  • Mathlib: DihedralGroup — Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
• Symmetric group — §1.3, Symmetric Groups, p. 29
  • Mathlib: Equiv.Perm — Mathlib/GroupTheory/Perm/Basic.lean
• Permutation — §1.3, Symmetric Groups, p. 29
  • Mathlib: Equiv.Perm — Mathlib/GroupTheory/Perm/Basic.lean
• General linear group — §1.4, Matrix Groups, p. 34
  • Mathlib: GL — Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean:47
• Quaternion group — §1.5, The Quaternion Group, p. 36
  • Mathlib: QuaternionGroup — Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
• Group homomorphism — §1.6, Homomorphisms and Isomorphisms, p. 36
  • Mathlib: MonoidHom — Mathlib/Algebra/Group/Hom/Defs.lean
• Group isomorphism — §1.6, Homomorphisms and Isomorphisms, p. 36
  • Mathlib: MulEquiv — Mathlib/Algebra/Group/Equiv/Defs.lean
• Group action — §1.7, Group Actions, p. 41
  • Mathlib: MulAction — Mathlib/GroupTheory/GroupAction/Defs.lean
• Permutation representation — §1.7, Group Actions, p. 41
  • Mathlib: MulAction.toPerm — Mathlib/GroupTheory/GroupAction/Basic.lean

Chapter 2: Subgroups

• Subgroup — §2.1, Definition and Examples, p. 46
  • Mathlib: Subgroup — Mathlib/Algebra/Group/Subgroup/Defs.lean
• Centralizer — §2.2, Centralizers and Normalizers, Stabilizers and Kernels, p. 49
  • Mathlib: Subgroup.centralizer — Mathlib/GroupTheory/Subgroup/Centralizer.lean
• Normalizer — §2.2, Centralizers and Normalizers, Stabilizers and Kernels, p. 49
  • Mathlib: Subgroup.normalizer — Mathlib/Algebra/Group/Subgroup/Defs.lean
• Stabilizer — §2.2, Centralizers and Normalizers, Stabilizers and Kernels, p. 49
  • Mathlib: MulAction.stabilizer — Mathlib/GroupTheory/GroupAction/Defs.lean
• Kernel of an action — §2.2, Centralizers and Normalizers, Stabilizers and Kernels, p. 49
  • Mathlib: MulAction.ker — Mathlib/GroupTheory/GroupAction/Defs.lean
• Cyclic group — §2.3, Cyclic Groups and Cyclic Subgroups, p. 54
  • Mathlib: Subgroup.zpowers — Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean:30
• Generated subgroup — §2.4, Subgroups Generated by Subsets of a Group, p. 61
  • Mathlib: Subgroup.closure — Mathlib/Algebra/Group/Subgroup/Lattice.lean:329
• Subgroup lattice — §2.5, The Lattice of Subgroups of a Group, p. 66
  • Mathlib: Subgroup — Mathlib/Algebra/Group/Subgroup/Lattice.lean

Chapter 3: Quotient Groups and Homomorphisms

• Left coset — §3.1, Definitions and Examples, p. 73
  • Mathlib: LeftCosetEquivalence — Mathlib/GroupTheory/Coset/Basic.lean
• Right coset — §3.1, Definitions and Examples, p. 73
  • Mathlib: RightCosetEquivalence — Mathlib/GroupTheory/Coset/Basic.lean
• Normal subgroup — §3.1, Definitions and Examples, p. 73
  • Mathlib: Subgroup.Normal — Mathlib/Algebra/Group/Subgroup/Defs.lean:605
• Quotient group — §3.1, Definitions and Examples, p. 73
  • Mathlib: QuotientGroup — Mathlib/GroupTheory/QuotientGroup/Defs.lean
• Index of a subgroup — §3.2, More on Cosets and Lagrange’s Theorem, p. 89
  • Mathlib: Subgroup.index — Mathlib/GroupTheory/Index.lean
• Composition series — §3.4, Composition Series and the Holder Program, p. 101
  • Mathlib: CompositionSeries — Mathlib/Order/JordanHolder.lean:137
• Simple group — §3.4, Composition Series and the Holder Program, p. 101
  • Mathlib: IsSimpleGroup — Mathlib/GroupTheory/Subgroup/Simple.lean:38
• Refinement of a composition series — §3.4, Composition Series and the Holder Program, p. 101
  • Mathlib: LTSeries.exists_relSeries_covBy — Mathlib/Order/RelSeries.lean
• Transposition — §3.5, Transpositions and the Alternating Group, p. 106
  • Mathlib: Equiv.swap — Mathlib/Logic/Equiv/Basic.lean
• Alternating group — §3.5, Transpositions and the Alternating Group, p. 106
  • Mathlib: alternatingGroup — Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Chapter 4: Group Actions

• Orbit — §4.1, Group Actions and Permutation Representations, p. 112
  • Mathlib: MulAction.orbit — Mathlib/GroupTheory/GroupAction/Defs.lean
• Faithful action — §4.1, Group Actions and Permutation Representations, p. 112
  • Mathlib: FaithfulSMul — Mathlib/GroupTheory/GroupAction/Defs.lean
• Regular action — §4.2, Groups Acting on Themselves by Left Multiplication, p. 118
  • Mathlib: Monoid.toMulAction — Mathlib/Algebra/Group/Action/Defs.lean
• Conjugation action — §4.3, Groups Acting on Themselves by Conjugation, p. 122
  • Mathlib: MulAction.conj — Mathlib/GroupTheory/GroupAction/ConjAct.lean
• Conjugacy class — §4.3, Groups Acting on Themselves by Conjugation, p. 122
  • Mathlib: conjugacyClass — (no Mathlib declaration; closest: IsConj — Mathlib/Algebra/Group/Conj.lean:32)
• Automorphism — §4.4, Automorphisms, p. 133
  • Mathlib: MulAut — Mathlib/Algebra/Group/End.lean:631
• Inner automorphism — §4.4, Automorphisms, p. 133
  • Mathlib: MulAut.inner — Mathlib/GroupTheory/GroupAction/ConjAct.lean
• Outer automorphism group — §4.4, Automorphisms, p. 133
  • LeanCategories: LeanCategories.Algebra.outerAutomorphismGroup — LeanCategories/Algebra/GroupTheory.lean
• p-subgroup — §4.5, The Sylow Theorems, p. 139
  • Mathlib: Sylow — Mathlib/GroupTheory/Sylow.lean
• Sylow p-subgroup — §4.5, The Sylow Theorems, p. 139
  • Mathlib: Sylow — Mathlib/GroupTheory/Sylow.lean

Chapter 5: Direct and Semidirect Products and Abelian Groups

• Direct product of groups — §5.1, Direct Products, p. 152
  • Mathlib: DirectProduct — (no Mathlib declaration; the product group is G × H with Prod.instGroup — Mathlib/Algebra/Group/Prod.lean:123)
• Finitely generated group — §5.2, The Fundamental Theorem of Finitely Generated Abelian Groups, p. 158
  • Mathlib: Monoid.FG — Mathlib/GroupTheory/Finiteness.lean:160
• Torsion subgroup — §5.2, The Fundamental Theorem of Finitely Generated Abelian Groups, p. 158
  • Mathlib: torsion — Mathlib/GroupTheory/Torsion.lean
• Invariant factors — §5.2, The Fundamental Theorem of Finitely Generated Abelian Groups, p. 158
  • LeanCategories: LeanCategories.Algebra.InvariantFactorData — LeanCategories/Algebra/CanonicalForms.lean
• Elementary divisors — §5.2, The Fundamental Theorem of Finitely Generated Abelian Groups, p. 158
  • Mathlib: Module.equiv_directSum_of_isTorsion — Mathlib/Algebra/Module/PID.lean
• Internal direct product — §5.4, Recognizing Direct Products, p. 169
  • Mathlib: Subgroup.internalDirectProduct — (no Mathlib declaration; closest: Subgroup.prod — Mathlib/Algebra/Group/Subgroup/Basic.lean:91)
• Semidirect product — §5.5, Semidirect Products, p. 175
  • Mathlib: SemidirectProduct — Mathlib/GroupTheory/SemidirectProduct.lean

Chapter 6: Further Topics in Group Theory

• p-group — §6.1, p-groups, Nilpotent Groups, and Solvable Groups, p. 188
  • Mathlib: IsPGroup — Mathlib/GroupTheory/Sylow.lean
• Upper central series — §6.1, p-groups, Nilpotent Groups, and Solvable Groups, p. 188
  • Mathlib: upperCentralSeries — Mathlib/GroupTheory/Nilpotent.lean:182
• Nilpotent group — §6.1, p-groups, Nilpotent Groups, and Solvable Groups, p. 188
  • Mathlib: IsNilpotent — Mathlib/GroupTheory/Nilpotent.lean
• Derived series — §6.1, p-groups, Nilpotent Groups, and Solvable Groups, p. 188
  • Mathlib: derivedSeries — Mathlib/GroupTheory/Solvable.lean:43
• Solvable group — §6.1, p-groups, Nilpotent Groups, and Solvable Groups, p. 188
  • Mathlib: IsSolvable — Mathlib/GroupTheory/Solvable.lean
• Free group — §6.3, A Word on Free Groups, p. 215
  • Mathlib: FreeGroup — Mathlib/GroupTheory/FreeGroup/Basic.lean:471
• Group presentation — §6.3, A Word on Free Groups, p. 215
  • Mathlib: PresentedGroup — Mathlib/GroupTheory/PresentedGroup.lean

Chapter 7: Introduction to Rings

• Ring — §7.1, Basic Definitions and Examples, p. 223
  • Mathlib: Ring — Mathlib/Algebra/Ring/Defs.lean
• Commutative ring — §7.1, Basic Definitions and Examples, p. 223
  • Mathlib: CommRing — Mathlib/Algebra/Ring/Defs.lean
• Ring with identity — §7.1, Basic Definitions and Examples, p. 223
  • Mathlib: Ring — Mathlib/Algebra/Ring/Defs.lean
• Unit — §7.1, Basic Definitions and Examples, p. 223
  • Mathlib: IsUnit — Mathlib/Algebra/Group/Units/Defs.lean:364
• Zero divisor — §7.1, Basic Definitions and Examples, p. 223
  • Mathlib: notMem_nonZeroDivisors_iff — Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
• Integral domain — §7.1, Basic Definitions and Examples, p. 223
  • Mathlib: IsDomain — Mathlib/Algebra/Ring/Defs.lean:439
• Division ring — §7.1, Basic Definitions and Examples, p. 223
  • Mathlib: DivisionRing — Mathlib/Algebra/Field/Defs.lean
• Field — §7.1, Basic Definitions and Examples, p. 223
  • Mathlib: Field — Mathlib/Algebra/Field/Defs.lean
• Subring — §7.1, Basic Definitions and Examples, p. 223
  • Mathlib: Subring — Mathlib/Algebra/Ring/Subring/Defs.lean
• Polynomial ring — §7.2, Polynomial Rings, Matrix Rings, and Group Rings, p. 233
  • Mathlib: Polynomial — Mathlib/Algebra/Polynomial/Basic.lean
• Matrix ring — §7.2, Polynomial Rings, Matrix Rings, and Group Rings, p. 233
  • Mathlib: Matrix — Mathlib/LinearAlgebra/Matrix/Defs.lean:55
• Group ring — §7.2, Polynomial Rings, Matrix Rings, and Group Rings, p. 233
  • Mathlib: MonoidAlgebra — Mathlib/Algebra/MonoidAlgebra/Defs.lean
• Ring homomorphism — §7.3, Ring Homomorphisms and Quotient Rings, p. 239
  • Mathlib: RingHom — Mathlib/Algebra/Ring/Hom/Defs.lean
• Ideal — §7.3, Ring Homomorphisms and Quotient Rings, p. 239
  • Mathlib: Ideal — Mathlib/RingTheory/Ideal/Defs.lean
• Quotient ring — §7.3, Ring Homomorphisms and Quotient Rings, p. 239
  • Mathlib: Ideal.Quotient — Mathlib/RingTheory/Ideal/Quotient/Defs.lean:43
• Prime ideal — §7.4, Properties of Ideals, p. 251
  • Mathlib: Ideal.IsPrime — Mathlib/RingTheory/Ideal/Prime.lean
• Maximal ideal — §7.4, Properties of Ideals, p. 251
  • Mathlib: Ideal.IsMaximal — Mathlib/RingTheory/Ideal/Operations.lean
• Ring of fractions — §7.5, Rings of Fractions, p. 260
  • Mathlib: Localization — Mathlib/RingTheory/Localization/Basic.lean

Chapter 8: Euclidean Domains, Principal Ideal Domains and Unique Factorization Domains

• Norm on an integral domain — §8.1, Euclidean Domains, p. 270
  • Mathlib: EuclideanDomain.norm — Mathlib/RingTheory/EuclideanDomain.lean
• Euclidean domain — §8.1, Euclidean Domains, p. 270
  • Mathlib: EuclideanDomain — Mathlib/RingTheory/EuclideanDomain.lean
• Principal ideal domain — §8.2, Principal Ideal Domains, p. 279
  • Mathlib: IsPrincipalIdealRing — Mathlib/RingTheory/PrincipalIdealDomain.lean
• Irreducible element — §8.3, Unique Factorization Domains, p. 283
  • Mathlib: Irreducible — Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
• Prime element — §8.3, Unique Factorization Domains, p. 283
  • Mathlib: Prime — Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
• Unique factorization domain — §8.3, Unique Factorization Domains, p. 283
  • Mathlib: UniqueFactorizationMonoid — Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

Chapter 9: Polynomial Rings

• Polynomial — §9.1, Definitions and Basic Properties, p. 295
  • Mathlib: Polynomial — Mathlib/Algebra/Polynomial/Basic.lean
• Degree of a polynomial — §9.1, Definitions and Basic Properties, p. 295
  • Mathlib: Polynomial.degree — Mathlib/Algebra/Polynomial/Degree/Definitions.lean
• Polynomial evaluation homomorphism — §9.1, Definitions and Basic Properties, p. 295
  • Mathlib: Polynomial.eval₂RingHom — Mathlib/Algebra/Polynomial/Eval/Defs.lean
• Content of a polynomial — §9.3, Polynomial Rings that are Unique Factorization Domains, p. 303
  • Mathlib: Polynomial.content — Mathlib/RingTheory/Polynomial/Content.lean:90
• Primitive polynomial — §9.3, Polynomial Rings that are Unique Factorization Domains, p. 303
  • Mathlib: Polynomial.IsPrimitive — Mathlib/RingTheory/Polynomial/Content.lean:45
• Eisenstein polynomial — §9.4, Irreducibility Criteria, p. 307
  • Mathlib: Polynomial.Eisenstein — Mathlib/Algebra/Polynomial/Eval/Defs.lean
• Multivariable polynomial ring — §9.6, Polynomials in Several Variables over a Field and Grobner Bases, p. 315
  • Mathlib: MvPolynomial — Mathlib/Algebra/MvPolynomial/Basic.lean:82
• Monomial order — §9.6, Polynomials in Several Variables over a Field and Grobner Bases, p. 315
  • Mathlib: MonomialOrder — Mathlib/Data/Finsupp/MonomialOrder.lean:61 (renamed from MvPolynomial.Order)
• Leading term — §9.6, Polynomials in Several Variables over a Field and Grobner Bases, p. 315
  • Mathlib: MonomialOrder.leadingCoeff — Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean:113 (renamed from MvPolynomial.leadingCoeff)
• Grobner basis — §9.6, Polynomials in Several Variables over a Field and Grobner Bases, p. 315
  • LeanCategories: MonomialOrder.IsGroebnerBasis — LeanCategories/Algebra/Polynomial.lean

Chapter 10: Introduction to Module Theory

• Left module — §10.1, Basic Definitions and Examples, p. 337
  • Mathlib: Module — Mathlib/Algebra/Module/Defs.lean
• Right module — §10.1, Basic Definitions and Examples, p. 337
  • Mathlib: Module — Mathlib/Algebra/Module/Defs.lean
• Submodule — §10.1, Basic Definitions and Examples, p. 337
  • Mathlib: Submodule — Mathlib/Algebra/Module/Submodule/Defs.lean
• Module homomorphism — §10.2, Quotient Modules and Module Homomorphisms, p. 345
  • Mathlib: LinearMap — Mathlib/Algebra/Module/LinearMap/Defs.lean:85
• Quotient module — §10.2, Quotient Modules and Module Homomorphisms, p. 345
  • Mathlib: Submodule.Quotient — Mathlib/Algebra/Module/Submodule/Basic.lean
• Generated submodule — §10.3, Generation of Modules, Direct Sums, and Free Modules, p. 351
  • Mathlib: Submodule.span — Mathlib/LinearAlgebra/Span/Defs.lean:48
• Finitely generated module — §10.3, Generation of Modules, Direct Sums, and Free Modules, p. 351
  • Mathlib: Module.Finite — Mathlib/RingTheory/Finiteness/Defs.lean
• Direct sum of modules — §10.3, Generation of Modules, Direct Sums, and Free Modules, p. 351
  • Mathlib: DirectSum — Mathlib/Algebra/DirectSum/Basic.lean
• Free module — §10.3, Generation of Modules, Direct Sums, and Free Modules, p. 351
  • Mathlib: Module.Free — Mathlib/LinearAlgebra/FreeModule/Basic.lean
• Tensor product — §10.4, Tensor Products of Modules, p. 359
  • Mathlib: TensorProduct — Mathlib/LinearAlgebra/TensorProduct/Defs.lean
• Exact sequence — §10.5, Exact Sequences: Projective, Injective, and Flat Modules, p. 378
  • Mathlib: Function.Exact — Mathlib/Algebra/Exact/Basic.lean
• Projective module — §10.5, Exact Sequences: Projective, Injective, and Flat Modules, p. 378
  • Mathlib: Module.Projective — Mathlib/Algebra/Module/Projective.lean
• Injective module — §10.5, Exact Sequences: Projective, Injective, and Flat Modules, p. 378
  • Mathlib: Module.Injective — Mathlib/Algebra/Module/Injective.lean
• Flat module — §10.5, Exact Sequences: Projective, Injective, and Flat Modules, p. 378
  • Mathlib: Module.Flat — Mathlib/RingTheory/Flat/Basic.lean

Chapter 11: Vector Spaces

• Vector space — §11.1, Definitions and Basic Theory, p. 408
  • Mathlib: Module — Mathlib/Algebra/Module/Defs.lean
• Linear transformation — §11.1, Definitions and Basic Theory, p. 408
  • Mathlib: LinearMap — Mathlib/Algebra/Module/LinearMap/Defs.lean:85
• Linear independence — §11.1, Definitions and Basic Theory, p. 408
  • Mathlib: LinearIndependent — Mathlib/LinearAlgebra/LinearIndependent/Defs.lean:98
• Basis — §11.1, Definitions and Basic Theory, p. 408
  • Mathlib: Basis — Mathlib/LinearAlgebra/Basis/Basic.lean
• Dimension — §11.1, Definitions and Basic Theory, p. 408
  • Mathlib: Module.finrank — Mathlib/LinearAlgebra/Dimension/Finrank.lean
• Matrix of a linear transformation — §11.2, The Matrix of a Linear Transformation, p. 415
  • Mathlib: LinearMap.toMatrix — Mathlib/LinearAlgebra/Matrix/ToLin.lean
• Dual vector space — §11.3, Dual Vector Spaces, p. 431
  • Mathlib: Module.Dual — Mathlib/LinearAlgebra/Dual/Defs.lean
• Dual basis — §11.3, Dual Vector Spaces, p. 431
  • Mathlib: Basis.dual — Mathlib/LinearAlgebra/Dual/Basis.lean
• Determinant — §11.4, Determinants, p. 435
  • Mathlib: Matrix.det — Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
• Tensor algebra — §11.5, Tensor Algebras, Symmetric and Exterior Algebras, p. 441
  • Mathlib: TensorAlgebra — Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
• Symmetric algebra — §11.5, Tensor Algebras, Symmetric and Exterior Algebras, p. 441
  • Mathlib: SymmetricAlgebra — Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean
• Exterior algebra — §11.5, Tensor Algebras, Symmetric and Exterior Algebras, p. 441
  • Mathlib: ExteriorAlgebra — Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

Chapter 12: Modules over Principal Ideal Domains

• Torsion element — §12.1, The Basic Theory, p. 458
  • Mathlib: Module.IsTorsion — Mathlib/Algebra/Module/Torsion/Basic.lean:224
• Torsion module — §12.1, The Basic Theory, p. 458
  • Mathlib: Module.IsTorsion — Mathlib/Algebra/Module/Torsion/Basic.lean:224
• Annihilator of a module — §12.1, The Basic Theory, p. 458
  • Mathlib: Module.annihilator — Mathlib/Algebra/Module/Defs.lean
• Rational canonical form — §12.2, The Rational Canonical Form, p. 472
  • LeanCategories: LeanCategories.Algebra.rationalCanonicalMatrix — LeanCategories/Algebra/CanonicalForms.lean
• Similar matrices — §12.2, The Rational Canonical Form, p. 472
  • Mathlib: Matrix.Similar — (no Mathlib declaration for matrix similarity)
• Minimal polynomial — §12.2, The Rational Canonical Form, p. 472
  • Mathlib: minpoly — Mathlib/FieldTheory/Minpoly/Basic.lean
• Characteristic polynomial — §12.2, The Rational Canonical Form, p. 472
  • Mathlib: LinearMap.charpoly — Mathlib/LinearAlgebra/Charpoly/Basic.lean
• Jordan canonical form — §12.3, The Jordan Canonical Form, p. 491
  • LeanCategories: LeanCategories.Algebra.IsJordanCanonical — LeanCategories/Algebra/JordanCanonical.lean
• Generalized eigenspace — §12.3, The Jordan Canonical Form, p. 491
  • Mathlib: LinearMap.genEigenspace — Mathlib/LinearAlgebra/Eigenspace/Basic.lean
• Jordan block — §12.3, The Jordan Canonical Form, p. 491
  • LeanCategories: LeanCategories.Algebra.JordanBlock — LeanCategories/Algebra/JordanCanonical.lean

Chapter 13: Field Theory

• Field extension — §13.1, Basic Theory of Field Extensions, p. 510
  • Mathlib: Algebra — Mathlib/Algebra/Algebra/Basic.lean
• Degree of a field extension — §13.1, Basic Theory of Field Extensions, p. 510
  • Mathlib: finrank — Mathlib/LinearAlgebra/Dimension/Finrank.lean
• Algebraic element — §13.2, Algebraic Extensions, p. 520
  • Mathlib: IsIntegral — Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean:53
• Transcendental element — §13.2, Algebraic Extensions, p. 520
  • Mathlib: Transcendental — Mathlib/RingTheory/Algebraic/Defs.lean:49 (renamed from IsTranscendental)
• Algebraic extension — §13.2, Algebraic Extensions, p. 520
  • Mathlib: IsAlgebraic — Mathlib/RingTheory/Algebraic/Defs.lean:45
• Minimal polynomial — §13.2, Algebraic Extensions, p. 520
  • Mathlib: minpoly — Mathlib/FieldTheory/Minpoly/Basic.lean
• Constructible number — §13.3, Classical Straightedge and Compass Constructions, p. 531
  • Mathlib: IsConstructible — (no Mathlib declaration for constructible field elements)
• Splitting field — §13.4, Splitting Fields and Algebraic Closures, p. 536
  • Mathlib: Polynomial.IsSplittingField — Mathlib/FieldTheory/SplittingField/IsSplittingField.lean:47 (renamed from IsSplittingField)
• Algebraic closure — §13.4, Splitting Fields and Algebraic Closures, p. 536
  • Mathlib: Algebra.IsAlgebraic — Mathlib/RingTheory/Algebraic/Defs.lean:68
• Separable polynomial — §13.5, Separable and Inseparable Extensions, p. 545
  • Mathlib: Polynomial.Separable — Mathlib/FieldTheory/Separable.lean
• Separable extension — §13.5, Separable and Inseparable Extensions, p. 545
  • Mathlib: IsSeparable — Mathlib/FieldTheory/Separable.lean
• Purely inseparable extension — §13.5, Separable and Inseparable Extensions, p. 545
  • Mathlib: IsPurelyInseparable — Mathlib/FieldTheory/PurelyInseparable/Basic.lean
• Cyclotomic polynomial — §13.6, Cyclotomic Polynomials and Extensions, p. 552
  • Mathlib: cyclotomic — Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean:230
• Cyclotomic field — §13.6, Cyclotomic Polynomials and Extensions, p. 552
  • Mathlib: CyclotomicField — Mathlib/NumberTheory/Cyclotomic/Basic.lean:655

Chapter 14: Galois Theory

• Automorphism group of a field extension — §14.1, Basic Definitions, p. 558
  • Mathlib: IntermediateField.Aut — Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
• Galois extension — §14.1, Basic Definitions, p. 558
  • Mathlib: IsGalois — Mathlib/FieldTheory/Galois/Basic.lean
• Galois group — §14.1, Basic Definitions, p. 558
  • Mathlib: IntermediateField.Aut — Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
• Fixed field — §14.2, The Fundamental Theorem of Galois Theory, p. 567
  • Mathlib: IntermediateField.fixed — Mathlib/FieldTheory/Fixed.lean
• Finite field — §14.3, Finite Fields, p. 585
  • Mathlib: FiniteField — Mathlib/FieldTheory/Finite/Basic.lean
• Composite field — §14.4, Composite Extensions and Simple Extensions, p. 591
  • Mathlib: IntermediateField.adjoin — Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
• Simple extension — §14.4, Composite Extensions and Simple Extensions, p. 591
  • Mathlib: AdjoinSimple — Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
• Abelian extension — §14.5, Cyclotomic Extensions and Abelian Extensions over Q, p. 596
  • Mathlib: IsAbelian — Mathlib/FieldTheory/Galois/Basic.lean
• Solvable polynomial by radicals — §14.7, Solvable and Radical Extensions, p. 625
  • Mathlib: solvableByRad — Mathlib/FieldTheory/AbelRuffini.lean
• Radical extension — §14.7, Solvable and Radical Extensions, p. 625
  • Mathlib: IsRadical — (no Mathlib declaration; closest: solvableByRad — Mathlib/FieldTheory/AbelRuffini.lean:196)
• Transcendence basis — §14.9, Transcendental Extensions, Inseparable Extensions, Infinite Galois Groups, p. 645
  • Mathlib: Algebra.IsAlgebraic — Mathlib/RingTheory/Algebraic/Defs.lean:68
• Infinite Galois extension — §14.9, Transcendental Extensions, Inseparable Extensions, Infinite Galois Groups, p. 645
  • Mathlib: IsGalois — Mathlib/FieldTheory/Galois/Basic.lean

Chapter 15: Commutative Rings and Algebraic Geometry

• Noetherian ring — §15.1, Noetherian Rings and Affine Algebraic Sets, p. 656
  • Mathlib: IsNoetherianRing — Mathlib/RingTheory/Noetherian/Basic.lean
• Affine n-space — §15.1, Noetherian Rings and Affine Algebraic Sets, p. 656
  • Mathlib: AffineSpace — Mathlib/AlgebraicGeometry/AffineScheme.lean
• Affine algebraic set — §15.1, Noetherian Rings and Affine Algebraic Sets, p. 656
  • Mathlib: AlgebraicSet — Mathlib/RingTheory/Ideal/Operations.lean
• Coordinate ring — §15.1, Noetherian Rings and Affine Algebraic Sets, p. 656
  • Mathlib: Ideal.Quotient — Mathlib/RingTheory/Ideal/Quotient/Defs.lean:43
• Radical of an ideal — §15.2, Radicals and Affine Varieties, p. 673
  • Mathlib: Ideal.radical — Mathlib/RingTheory/Ideal/Operations.lean:799
• Affine variety — §15.2, Radicals and Affine Varieties, p. 673
  • Mathlib: AlgebraicSet — Mathlib/RingTheory/Ideal/Operations.lean
• Zariski topology — §15.2, Radicals and Affine Varieties, p. 673
  • Mathlib: PrimeSpectrum.instTopologicalSpace — Mathlib/RingTheory/Spectrum/Prime/Topology.lean
• Integral element — §15.3, Integral Extensions and Hilbert’s Nullstellensatz, p. 691
  • Mathlib: IsIntegral — Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean:53
• Integral extension — §15.3, Integral Extensions and Hilbert’s Nullstellensatz, p. 691
  • Mathlib: Algebra.IsIntegral — Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean:36
• Integral closure — §15.3, Integral Extensions and Hilbert’s Nullstellensatz, p. 691
  • Mathlib: integralClosure — Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean:215
• Localization of a ring — §15.4, Localization, p. 706
  • Mathlib: Localization — Mathlib/RingTheory/Localization/Basic.lean
• Localization of a module — §15.4, Localization, p. 706
  • Mathlib: LocalizedModule — Mathlib/RingTheory/Localization/Module.lean
• Local ring — §15.4, Localization, p. 706
  • Mathlib: IsLocalRing — Mathlib/RingTheory/LocalRing/Basic.lean
• Prime spectrum — §15.5, The Prime Spectrum of a Ring, p. 731
  • Mathlib: PrimeSpectrum — Mathlib/RingTheory/Spectrum/Prime/Defs.lean
• Structure sheaf — §15.5, The Prime Spectrum of a Ring, p. 731
  • Mathlib: Scheme.O — (no Mathlib declaration; closest: structureSheafInType — Mathlib/AlgebraicGeometry/StructureSheaf.lean:171)
• Stalk of the structure sheaf — §15.5, The Prime Spectrum of a Ring, p. 731
  • Mathlib: Presheaf.stalk — Mathlib/Topology/Sheaves/Stalks.lean

Chapter 16: Artinian Rings, Discrete Valuation Rings, and Dedekind Domains

• Artinian ring — §16.1, Artinian Rings, p. 750
  • Mathlib: IsArtinianRing — Mathlib/RingTheory/Artinian/Ring.lean
• Discrete valuation — §16.2, Discrete Valuation Rings, p. 755
  • Mathlib: Valuation — Mathlib/RingTheory/Valuation/ValuationSubring.lean
• Discrete valuation ring — §16.2, Discrete Valuation Rings, p. 755
  • Mathlib: IsDiscreteValuationRing — Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
• Dedekind domain — §16.3, Dedekind Domains, p. 764
  • Mathlib: IsDedekindDomain — Mathlib/RingTheory/DedekindDomain/Basic.lean
• Fractional ideal — §16.3, Dedekind Domains, p. 764
  • Mathlib: FractionalIdeal — Mathlib/RingTheory/FractionalIdeal/Basic.lean
• Ideal class group — §16.3, Dedekind Domains, p. 764
  • Mathlib: ClassGroup — Mathlib/RingTheory/ClassGroup/Basic.lean

Chapter 17: Introduction to Homological Algebra and Group Cohomology

• Chain complex — §17.1, Introduction to Homological Algebra: Ext and Tor, p. 777
  • Mathlib: ChainComplex — Mathlib/Algebra/Homology/HomologicalComplex.lean
• Chain map — §17.1, Introduction to Homological Algebra: Ext and Tor, p. 777
  • Mathlib: HomologicalComplex.Hom — Mathlib/Algebra/Homology/HomologicalComplex.lean
• Homology group — §17.1, Introduction to Homological Algebra: Ext and Tor, p. 777
  • Mathlib: ShortComplex.homology — Mathlib/Algebra/Homology/ShortComplex/Homology.lean:381 (renamed from Homology)
• Projective resolution — §17.1, Introduction to Homological Algebra: Ext and Tor, p. 777
  • Mathlib: ProjectiveResolution — Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean:41
• Injective resolution — §17.1, Introduction to Homological Algebra: Ext and Tor, p. 777
  • Mathlib: InjectiveResolution — Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean:43
• Ext group — §17.1, Introduction to Homological Algebra: Ext and Tor, p. 777
  • Mathlib: ModuleCat.Ext — Mathlib/Algebra/Category/ModuleCat/Ext/Basic.lean
• Tor group — §17.1, Introduction to Homological Algebra: Ext and Tor, p. 777
  • Mathlib: ModuleCat.Tor — (no Mathlib declaration; closest: CategoryTheory.Tor — Mathlib/CategoryTheory/Monoidal/Tor.lean:44)
• G-module — §17.2, The Cohomology of Groups, p. 798
  • Mathlib: Representation — Mathlib/RepresentationTheory/Basic.lean
• Group cohomology — §17.2, The Cohomology of Groups, p. 798
  • Mathlib: groupCohomology — Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean:187 (renamed from GroupCohomology)
• Crossed homomorphism — §17.3, Crossed Homomorphisms and H1(G,A), p. 814
  • Mathlib: IsCocycle₁ — Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
• Principal crossed homomorphism — §17.3, Crossed Homomorphisms and H1(G,A), p. 814
  • Mathlib: IsCoboundary₁ — Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean
• Group extension — §17.4, Group Extensions, Factor Sets and H2(G,A), p. 824
  • Mathlib: GroupExtension — Mathlib/GroupTheory/GroupExtension/Defs.lean:74
• Factor set — §17.4, Group Extensions, Factor Sets and H2(G,A), p. 824
  • Mathlib: IsMulCocycle₂ — Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean

Chapter 18: Representation Theory and Character Theory

• Representation of a group — §18.1, Linear Actions and Modules over Group Rings, p. 840
  • Mathlib: Representation — Mathlib/RepresentationTheory/Basic.lean
• Representation module — §18.1, Linear Actions and Modules over Group Rings, p. 840
  • Mathlib: Representation — Mathlib/RepresentationTheory/Basic.lean
• Subrepresentation — §18.1, Linear Actions and Modules over Group Rings, p. 840
  • Mathlib: Subrepresentation — Mathlib/RepresentationTheory/Basic.lean
• Irreducible representation — §18.1, Linear Actions and Modules over Group Rings, p. 840
  • Mathlib: IsIrreducible — Mathlib/RepresentationTheory/Basic.lean
• Completely reducible representation — §18.1, Linear Actions and Modules over Group Rings, p. 840
  • Mathlib: IsSemisimpleModule — Mathlib/RingTheory/SimpleModule/Basic.lean
• Semisimple ring — §18.2, Wedderburn’s Theorem and Some Consequences, p. 854
  • Mathlib: IsSemisimpleRing — Mathlib/RingTheory/SimpleModule/Basic.lean
• Character of a representation — §18.3, Character Theory and the Orthogonality Relations, p. 864
  • Mathlib: Character — Mathlib/RepresentationTheory/Character.lean
• Class function — §18.3, Character Theory and the Orthogonality Relations, p. 864
  • Mathlib: ClassFunction — Mathlib/RepresentationTheory/Character.lean
• Character inner product — §18.3, Character Theory and the Orthogonality Relations, p. 864
  • Mathlib: inner — Mathlib/RepresentationTheory/Character.lean

Chapter 19: Examples and Applications of Character Theory

• Character table — §19.1, Characters of Groups of Small Order, p. 880
  • Mathlib: CharacterTable — Mathlib/RepresentationTheory/Character.lean
• Induced representation — §19.3, Introduction to the Theory of Induced Characters, p. 892
  • Mathlib: InducedRepresentation — Mathlib/RepresentationTheory/Induced.lean
• Induced character — §19.3, Introduction to the Theory of Induced Characters, p. 892
  • Mathlib: InducedCharacter — Mathlib/RepresentationTheory/Induced.lean
• Restriction of a character — §19.3, Introduction to the Theory of Induced Characters, p. 892
  • Mathlib: Character.restrict — Mathlib/RepresentationTheory/Character.lean