Mathlib Map

Structures · Algebra

Algebra

An associative unital R-algebra is a semiring A equipped with a map into its center R → A. See the implementation notes in this file for discussion of the details of this definition.

Defined in
Mathlib.Algebra.Algebra.Defs
Shape
2 explicit arguments · adds algebraMap, commutes', smul_def'
Open in Mathlib docs

Extends1

Extended by2

Concrete types that are instances33

  • Int
  • Nat
  • Real
  • Rat
  • NNReal
  • ZMod
  • Polynomial
  • CommRingCat.carrier
  • RatFunc
  • NNRat
  • WithVal
  • PadicInt
  • IsLocalRing.ResidueField
  • Polynomial.SplittingField
  • Localization
  • AdjoinRoot
  • NumberField.RingOfIntegers
  • MvPowerSeries
  • CyclotomicRing
  • AlgebraicGeometry.ValuativeCommSq.R
  • HomogeneousLocalization
  • Algebra.Presentation.Core
  • PointedContMDiffMap
  • Algebra.Extension.Ring
  • MvPolynomial
  • PowerSeries
  • Localization.AtPrime
  • _private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.T
  • Algebra.Generators.Ring
  • Subtype
  • HasQuotient.Quotient
  • WithAbs
  • Ideal

How is a type an instance?

Loading the hierarchy index…

Assumed by13,924

Ancestors4