algebra
- archimedean
- associated
- big_operators
- char_p
- char_zero
- commute
- direct_limit
- euclidean_domain
- field
- floor
- gcd_domain
- geom_sum
- group_power
- module
- order
- order_functions
- ordered_group
- ordered_ring
- pi_instances
- quadratic_discriminant
- ring
- semiconj
- category
  - Group
  - CommRing
    - adjunctions
    - basic
    - colimits
    - limits
  - Module
    - basic
  - Mon
- continued_fractions
- group
  - anti_hom
  - hom
  - to_additive
  - type_tags
  - units
  - units_hom
algebraic_geometry
analysis
- convex
- calculus
- complex
- normed_space
category
- basic
- fold
- functor
- bitraversable
  - basic
  - instances
  - lemmas
- monad
  - basic
  - writer
- traversable
  - basic
  - derive
category_theory
- conj
- const
- core
- elements
- endomorphism
- eq_to_hom
- equivalence
- fully_faithful
- functor
- functor_category
- groupoid
- hom_functor
- isomorphism
- isomorphism_classes
- natural_isomorphism
- natural_transformation
- opposites
- pempty
- punit
- single_obj
- sparse
- types
- yoneda
- adjunction
  - basic
  - limits
- category
  - Cat
  - Groupoid
  - Rel
  - default
- concrete_category
- limits
  - cones
  - limits
  - preserves
  - shapes
    - binary_products
    - equalizers
    - finite_limits
    - products
    - pullbacks
    - constructions
      - limits_of_products_and_equalizers
- monad
  - adjunction
  - algebra
  - types
- monoidal
- products
  - basic
- sums
  - basic
computability
data
- dfinsupp
- erased
- fin
- finmap
- finset
- finsupp
- fintype
- hash_map
- holor
- multiset
- mv_polynomial
- opposite
- pequiv
- pfun
- polynomial
- prod
- quot
- semiquot
- setoid
- subtype
- sum
- tree
- vector2
- analysis
- equiv
  - algebra
  - basic
  - denumerable
  - encodable
  - list
  - local_equiv
- fintype
  - intervals
- int
  - basic
  - gcd
  - sqrt
- list
  - alist
  - basic
  - defs
  - min_max
  - perm
  - sigma
  - sort
- matrix
  - pequiv
- nat
  - basic
  - cast
  - choose
  - dist
  - enat
  - fib
  - gcd
  - modeq
  - pairing
  - prime
  - sqrt
- num
  - basic
- option
  - basic
  - defs
- padics
- pnat
  - basic
  - factors
  - xgcd
- rat
  - basic
  - cast
  - default
  - floor
  - meta_defs
  - order
- real
  - cau_seq
  - ennreal
  - hyperreal
  - nnreal
  - pi
- seq
  - computation
  - parallel
  - seq
  - wseq
- set
  - basic
  - countable
  - disjointed
  - finite
  - function
  - intervals
  - lattice
- sigma
  - basic
- string
  - defs
- zmod
  - basic
- zsqrtd
field_theory
geometry
- manifold
group_theory
- coset
- free_group
- group_action
- order_of_element
- presented_group
- quotient_group
- subgroup
- submonoid
- sylow
- perm
  - sign
linear_algebra
- basic
- basis
- bilinear_form
- dimension
- dual
- finite_dimensional
- finsupp
- matrix
- sesquilinear_form
logic
- basic
- embedding
- function
- relation
measure_theory
- giry_monad
- integration
- lebesgue_measure
- measurable_space
- measure_space
- outer_measure
- probability_mass_function
- category
  - Meas
meta
number_theory
order
- basic
- boolean_algebra
- bounded_lattice
- complete_boolean_algebra
- complete_lattice
- conditionally_complete_lattice
- fixed_points
- galois_connection
- lattice
- lexicographic
- liminf_limsup
- order_iso
- zorn
- filter
ring_theory
set_theory
- cardinal
- cofinality
- game
- ordinal
- ordinal_notation
- pgame
- surreal
- zfc
tactic
- abel
- apply
- apply_fun
- auto_cases
- cache
- chain
- core
- elide
- ext
- fin_cases
- finish
- generalize_proofs
- interactive
- lift
- linarith
- lint
- local_cache
- localized
- mk_iff_of_inductive_prop
- norm_cast
- norm_num
- pi_instances
- push_neg
- rcases
- reassoc_axiom
- replacer
- restate_axiom
- rewrite
- ring
- ring2
- scc
- simpa
- simps
- slice
- solve_by_elim
- split_ifs
- subtype_instance
- suggest
- tauto
- tfae
- well_founded_tactics
- wlog
- converter
  - interactive
- monotonicity
  - interactive
- omega
  - main
- rewrite_all
  - default
topology
- bases
- basic
- bounded_continuous_function
- compact_open
- constructions
- continuous_on
- dense_embedding
- homeomorph
- local_homeomorph
- maps
- opens
- order
- separation
- sequences
- stone_cech
- subset_properties
- topological_fiber_bundle
- algebra
  - group
  - infinite_sum
  - module
  - monoid
  - open_subgroup
  - ordered
  - ring
  - uniform_group
- category
  - TopCommRing
  - UniformSpace
  - Top
    - adjunctions
    - basic
    - opens
- instances
  - ennreal
- metric_space
- sheaves
- uniform_space