v1.10.0

• Tactics:

  • assumption meta
  • in meta
  • defaultImpl meta

• Sets and logic:

  • Pigeonhole principle
  • Kuratowski-finite sets
  • "The following are equivalent" proofs
  • Countable sets
  • Subset operations
  • Simplified syntax for quantifiers
  • Partial elements

• Algebra:

  • Graded rings homogeneous ideals homogeneous localizations, Proj construction
  • Lagrange's theorem
  • Dimension of a ring, a characterization of zero-dimensional rings, zero-dimensional local rings, and von Neumann regular rings
  • A characterization of Smith rings
  • PIDs are Smith domains
  • PIDs are 1-dimensional
  • Euclidean domains are PIDs
  • Polynomial division
  • Matrix ring
  • Various definitions of determinant and a proof that they are equivalent
  • Various properties of determinant
  • Symmetric group, its cardinality, sign homomorphism
  • Characteristic polynomial of a matrix and a proof that eigenvalues are its roots
  • Integral elements and extensions, a characterization of finitely generated integral extensions
  • Monoid rings and multivariate polynomials
  • Valuation rings
  • Factor rings and factor fields
  • Nakayama's lemma
  • The minimal polynomial of an element of a ring extension
  • A proof that a finitely generated extension is integral if and only if it is zero-dimensional
  • The Chinese remainder theorem
  • Dimension of a finite free module
  • Independent sets, bases, and their various properties
  • The image and the kernel of a linear map between finite modules over a Smith domain are finite
  • Linear dependency is decidable in a finite module over a Smith domain
  • Splitting fields of polynomials over countable fields
  • Rank of a matrix over a Smith domain
  • Surjective linear endomaps on a finitely generated module are bijective
  • Cayley-Hamilton theorem
  • Direct limits of algebraic structures over semilattices
  • Algebraically closed fields and the algebraic closure of a countable field
  • The absolute value for linearly ordered abelian groups
  • Group actions
  • First isomorphism theorem

• Topology:

  • Cover spaces
  • Completion of cover spaces
  • Uniform spaces and their completion
  • Metric spaces and their completion
  • Equivalence between appropriate subcategories of complete cover spaces and regular locales
  • Topological abeliean groups and their completion
  • Normed abelian groups, normed rings, Banach spaces
  • Products of topological spaces, cover spaces, uniform spaces, and topological abelian groups
  • Normed abelian group of real numbers
  • Compact spaces and a characteriization of cover maps
  • Cover space structure on directed sets

• Analysis:

  • Limit of a function on a directed set
  • Uniform convergence
  • Series and various convergence tests
  • Power series and their radius of convergence

• Real and complex numbers:

  • The field of real numbers
  • The field of complex numbers
  • The exponential function on real numbers

• Categories:

  • Heyting algebras
  • Cartesian closed categories
  • Elementary topoi