Mathlib Map

Structures · Lean core

Pow

The homogeneous version of HPow: a ^ b : α where a : α, b : β. (The right argument is not the same as the left since we often want this even in the homogeneous case.) Types can choose to subscribe to particular defaulting behavior by providing an instance to either NatPow or HomogeneousPow: - NatPow is for types whose exponents is preferentially a Nat. - HomogeneousPow is for types whose base and exponent are preferentially the same.

Defined in
Init.Prelude
Shape
2 explicit arguments · adds pow
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Forgetful instances

Every Pow is also a

Provided automatically by

Concrete types that are instances81

  • Real
  • Rat
  • Quiver.Hom
  • Complex
  • SeparationQuotient
  • NNReal
  • BitVec
  • ENNReal
  • Polynomial
  • Filter.Germ
  • BoundedContinuousFunction
  • UInt64
  • NNRat
  • UInt8
  • UInt16
  • UInt32
  • WithConv
  • WithVal
  • NonemptyInterval
  • LocallyConstant
  • USize
  • ENat
  • Units
  • MeasureTheory.SimpleFunc
  • RestrictedProduct
  • TrivSqZeroExt
  • UniformFun
  • DoubleCentralizer
  • UniformOnFun
  • CauSeq.Completion.Cauchy
  • ContMDiffMap
  • Int32
  • Int8
  • Int64
  • Int16
  • WittVector
  • CauSeq
  • TruncatedWittVector
  • Tropical
  • Ordinal
  • FractionalIdeal
  • AdicCompletion
  • Matrix.SpecialLinearGroup
  • Cardinal
  • MeasureTheory.AEEqFun
  • ISize
  • Representation.IntertwiningMap
  • AdicCompletion.AdicCauchySequence
  • RingCon.Quotient
  • HomogeneousLocalization
  • AlgebraicGeometry.Scheme.IdealSheafData
  • CentroidHom
  • Equiv.Perm
  • OneHom
  • Complex.UnitClosedDisc
  • CategoryTheory.Equivalence
  • Complex.UnitDisc
  • GroupLike
  • Dyadic
  • SpecialLinearGroup
  • Con.Quotient
  • AddConstEquiv
  • ONote
  • HomogeneousLocalization.NumDenSameDeg
  • AddConstMap
  • RegularExpression
  • Mathlib.Tactic.FieldSimp.NF
  • Subtype
  • Prod
  • OrderDual
  • Set.Elem
  • ULift
  • Fin
  • Lex
  • AddOpposite
  • ContinuousMap
  • Shrink
  • Colex
  • Submodule
  • WithZero
  • MonoidHom

How is a type an instance?

Loading the hierarchy index…

Assumed by236

Ancestors3