Map · 08
general algebraic systems
MSC 08 · General algebraic systems
1,245 declarations (1,043 theorems, 202 definitions) across 28 files. The 1000+ theorems list has no entries in this area. 2 open conjectures here are stated in Lean.
Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.
Subareas1
- 08A Algebraic structures 1,245
Open conjectures stated in Lean2
Statements without proofs, collected by the Formal Conjectures project.
Structures defined here18
Typeclasses defined in this area's files, most assumed first.
Files28
Largest first. The code after each file is its assigned subarea.
- Mathlib.Data.Finsupp.Basic
Miscellaneous definitions, lemmas, and constructions using finsupp
08A · 246
- Mathlib.Data.DFinsupp.Defs
Dependent functions with finite support
08A · 222
- Mathlib.Data.Finsupp.Defs
Type of functions with finite support
08A · 98
- Mathlib.Algebra.Notation.Support
Support of a function
08A · 86
- Mathlib.Data.DFinsupp.BigOperators
Dependent functions with finite support
08A · 86
- Mathlib.Data.Finsupp.Single
Finitely supported functions on exactly one point
08A · 84
- Mathlib.Data.FunLike.IsApply
Typeclasses for `FunLike` and algebraic operations
08A · 83
- Mathlib.Data.Finsupp.ToDFinsupp
Conversion between `Finsupp` and homogeneous `DFinsupp`
08A · 42
- Mathlib.Algebra.Notation.Pi.Basic
Very basic algebraic operations on pi types
08A · 38
- Mathlib.Data.Finsupp.Option
Operations on `Finsupp`s with an `Option` domain
08A · 29
- Mathlib.Data.Finsupp.SMul
Declarations about scalar multiplication on `Finsupp`
08A · 26
- Mathlib.Data.DFinsupp.NeLocus
Locus of unequal values of finitely supported dependent functions
08A · 25