WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Exponentiation

Revision #1210 → #1825 · back to history

modifiedExponentiation (positive integer exponent)b8fc6a52cb1b
FieldFrom #1210To #1825
anchors[{"section":"(Lead)","snippet":"When n is a positive integer , exponentiation corresponds to repeated multiplication of the base"},{"type":"math_alttext","value":"{\\displaystyle b^{n}=\\underbrace {b\\times b\\times \\dots \\times b\\times b} _{n{\\text{ times}}}.}"}]—
modifiedMultiplication rule for exponentsd0795ace5313
FieldFrom #1210To #1825
anchors[{"section":"(Lead)","snippet":"the multiplication rule"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}b^{n}\\times b^{m}&=\\underbrace {b\\times \\dots \\times b} _{n{\\text{ times}}}\\times \\underbrace {b\\times \\dots \\times b} _{m{\\text{ times}}}\\\\[1ex]&=\\underbrace {b\\times \\dots \\times b} _{n+m{\\text{ times}}}=b^{n+m}.\\end{aligned}}}"}]—
mathlib.moduleMathlib.Algebra.GroupPower.BasicMathlib.Algebra.Group.Defs
modifiedZeroth, negative, and fractional powers649819e3e1bf
FieldFrom #1210To #1825
anchors[{"section":"(Lead)","snippet":"Exponentiation can also be extended to powers that are not positive integers"},{"type":"math_alttext","value":"{\\displaystyle b^{0}=1}"},{"type":"math_alttext","value":"{\\displaystyle b^{-n}=1/b^{n},}"},{"type":"math_alttext","value":"{\\displaystyle b^{n/m}={\\sqrt[{m}]{b^{n}}}}"}]—
modifiedArchimedes' law of exponents for powers of tencae51c3b8666
FieldFrom #1210To #1825
mathlib.moduleMathlib.Algebra.GroupPower.BasicMathlib.Algebra.Group.Defs
modifiedSquare of be1e3aa6e882b
FieldFrom #1210To #1825
mathlib.moduleMathlib.Algebra.GroupPower.BasicMathlib.Algebra.Group.Defs
modifiedAssociativity gives exponent product rule8345eea4058f
FieldFrom #1210To #1825
mathlib.moduleMathlib.Algebra.GroupPower.BasicMathlib.Algebra.Group.Defs
modifiedNegative integer exponents3e2b607a0268
FieldFrom #1210To #1825
mathlib.moduleMathlib.Algebra.Group.DefsMathlib.Algebra.Group.Basic
modifiedAlternating sign of powers of -1d0fd6a7cd129
FieldFrom #1210To #1825
mathlib.moduleMathlib.Algebra.GroupPower.BasicMathlib.Algebra.Ring.Commute
modifiedExponential function (limit definition)c1eb40e25a6c
FieldFrom #1210To #1825
mathlib.moduleMathlib.Data.Complex.ExponentialMathlib.Analysis.Complex.Exponential
note`Real.exp` is defined via the power series; the `(1+x/n)^n` limit form is not the primary definition in Mathlib.`Real.exp` is defined via the power series; the `(1+x/n)^n` limit form is proved equivalent via `Real.tendsto_one_add_div_pow_exp`.
modifiedExponential identitya1b60836b59e
FieldFrom #1210To #1825
mathlib.moduleMathlib.Data.Complex.ExponentialMathlib.Analysis.Complex.Exponential
modifiedEuler's numberc7fea11fa08c
FieldFrom #1210To #1825
mathlib.declReal.exp_oneReal.exp
mathlib.match_kindexactinvocation
mathlib.moduleMathlib.Data.Complex.ExponentialMathlib.Analysis.Complex.Exponential
noteMathlib uses `Real.exp 1` for Euler's number; `Real.exp_one_pos` etc.Mathlib has no dedicated `Real.e` constant; Euler's number is `Real.exp 1`, with numerical bounds like `Real.exp_one_gt_two`.
modifiedExtension of exp to complex arguments1e59c51c893c
FieldFrom #1210To #1825
mathlib.moduleMathlib.Data.Complex.ExponentialMathlib.Analysis.Complex.Exponential
modifiedEuler's formulaf32376a5aeb9
FieldFrom #1210To #1825
mathlib.moduleMathlib.Analysis.SpecialFunctions.Complex.CircleMathlib.Analysis.Complex.Trigonometric
modifiedPolar form of a complex number650e2688c4d3
FieldFrom #1210To #1825
mathlib.declComplex.abs_mul_exp_arg_mul_IComplex.norm_mul_exp_arg_mul_I
mathlib.moduleMathlib.Analysis.SpecialFunctions.Complex.CircleMathlib.Analysis.SpecialFunctions.Complex.Arg
note`Complex.abs_mul_exp_arg_mul_I` writes `z = ‖z‖ * exp(arg z * I)`.`Complex.norm_mul_exp_arg_mul_I` writes `z = ‖z‖ * exp(arg z * I)`.
modifiedn distinct n th roots of a complex numberf278491112b6
FieldFrom #1210To #1825
mathlib.declComplex.card_nthRootsIsPrimitiveRoot.card_nthRoots
mathlib.moduleMathlib.Analysis.SpecialFunctions.Complex.CircleMathlib.RingTheory.RootsOfUnity.PrimitiveRoots
note`Complex.card_nthRoots` (and `Polynomial.card_nthRoots`) give the n distinct roots.`IsPrimitiveRoot.card_nthRoots` gives that `nthRoots n a` has cardinality `n` (when a root exists).
modifiedPrimitive n th roots of unity74ae646f4462
FieldFrom #1210To #1825
mathlib.moduleMathlib.RingTheory.RootsOfUnity.BasicMathlib.RingTheory.RootsOfUnity.PrimitiveRoots
modifiedn th roots via roots of unity27bdda34c05a
FieldFrom #1210To #1825
mathlib.moduleMathlib.RingTheory.RootsOfUnity.BasicMathlib.RingTheory.RootsOfUnity.PrimitiveRoots
modifiedValues of i^i0c4f8e6abf41
FieldFrom #1210To #1825
anchors[{"section":"Computation","snippet":"The polar form of i is"},{"type":"math_alttext","value":"{\\displaystyle \\log i=i\\left({\\frac {\\pi }{2}}+2k\\pi \\right).}"},{"type":"math_alttext","value":"{\\displaystyle i^{i}=e^{i\\log i}=e^{-{\\frac {\\pi }{2}}}e^{-2k\\pi }.}"},{"type":"math_alttext","value":"{\\displaystyle e^{-{\\frac {\\pi }{2}}}\\approx 0.2079.}"}]—
modifiedValues of (-2)^wa3e28737f8ee
FieldFrom #1210To #1825
anchors[{"section":"Computation","snippet":"the polar form of −2 is"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}(-2)^{3+4i}&=2^{3}e^{-4(\\pi +2k\\pi )}(\\cos(4\\ln 2+3(\\pi +2k\\pi ))+i\\sin(4\\ln 2+3(\\pi +2k\\pi )))\\\\&=-2^{3}e^{-4(\\pi +2k\\pi )}(\\cos(4\\ln 2)+i\\sin(4\\ln 2)).\\end{aligned}}}"}]—
modifiedFailure of log(b^x)=x log b for complex5e32e3e4bae0
FieldFrom #1210To #1825
anchors[{"section":"Failure of power and logarithm identities","snippet":"The identity log( b x ) = x ⋅ log b holds whenever b is a positive real number"},{"type":"math_alttext","value":"{\\displaystyle \\log((-i)^{2})=\\log(-1)=i\\pi \\neq 2\\log(-i)=2\\log(e^{-i\\pi /2})=2\\,{\\frac {-i\\pi }{2}}=-i\\pi }"},{"type":"math_alttext","value":"{\\displaystyle \\log w^{z}\\equiv z\\log w{\\pmod {2\\pi i}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\left\\{\\log w^{z}\\right\\}&=\\left\\{z\\cdot \\operatorname {Log} w+z\\cdot 2\\pi in+2\\pi im\\mid m,n\\in \\mathbb {Z} \\right\\}\\\\\\left\\{z\\log w\\right\\}&=\\left\\{z\\operatorname {Log} w+z\\cdot 2\\pi in\\mid n\\in \\mathbb {Z} \\right\\}\\end{aligned}}}"}]—
modifiedFailure of (bc)^x = b^x c^x for complexe1127501188f
FieldFrom #1210To #1825
anchors[{"section":"Failure of power and logarithm identities","snippet":"The identities ( bc ) x = b x c x and ( b / c ) x = b x / c x are valid"},{"type":"math_alttext","value":"{\\displaystyle (-1\\cdot -1)^{\\frac {1}{2}}=1\\neq (-1)^{\\frac {1}{2}}(-1)^{\\frac {1}{2}}=i\\cdot i=i^{2}=-1}"},{"type":"math_alttext","value":"{\\displaystyle \\left({\\frac {1}{-1}}\\right)^{\\frac {1}{2}}=(-1)^{\\frac {1}{2}}=i\\neq {\\frac {1^{\\frac {1}{2}}}{(-1)^{\\frac {1}{2}}}}={\\frac {1}{i}}=-i}"}]—
modifiedAlgebraic base, rational exponent gives algebraic131a33a7d52a
FieldFrom #1210To #1825
mathlib.moduleMathlib.RingTheory.Algebraic.BasicMathlib.RingTheory.Algebraic.Integral
modifiedConjugation notation0b9804e7e594
FieldFrom #1210To #1825
mathlib.declCommute.conj_powconj_pow
mathlib.moduleMathlib.Algebra.Group.Semiconj.UnitsMathlib.Algebra.Group.Conj
noteMathlib has `conj_pow` lemmas but no `x^y` conjugation notation.Mathlib has `conj_pow` (and `Units.conj_pow`) but no `x^y` conjugation notation per se.
modifiedNilpotent element6d73a6b20198
FieldFrom #1210To #1825
mathlib.moduleMathlib.RingTheory.Nilpotent.DefsMathlib.Algebra.GroupWithZero.Basic
modifiedReduced ringf0d32b658105
FieldFrom #1210To #1825
mathlib.moduleMathlib.RingTheory.Nilpotent.DefsMathlib.Algebra.GroupWithZero.Basic
modifiedMatrix power7ea7c89cd85c
FieldFrom #1210To #1825
mathlib.declMatrix.pow_eqMonoid.npow
mathlib.match_kindexactinvocation
mathlib.moduleMathlib.LinearAlgebra.Matrix.ZPowMathlib.Algebra.Group.Defs
noteSquare matrices form a monoid, so `A^n` is given by `Monoid.npow`; `Matrix.zpow` for integer exponents.Square matrices form a monoid, so `A^n` is given by `Monoid.npow`; many `Matrix.*_pow` lemmas exist.
modifiedPrimitive element of a finite fieldebe7f86da493
FieldFrom #1210To #1825
mathlib.declFiniteField.isCyclicinstIsCyclicUnitsOfFinite
mathlib.moduleMathlib.FieldTheory.Finite.BasicMathlib.RingTheory.IntegralDomain
noteMathlib proves the unit group is cyclic, implying a primitive element exists; no `primitiveElement` decl specific to finite fields.`instIsCyclicUnitsOfFinite` shows the unit group of any finite integral domain (incl. finite fields) is cyclic, so a primitive element exists; no `primitiveElement` decl specific to finite fields.
modifiedFrobenius automorphism8ab3b2424c8d
FieldFrom #1210To #1825
mathlib.moduleMathlib.Algebra.CharP.FrobeniusMathlib.Algebra.CharP.Lemmas
modifiedGalois group of finite field extensionda5709b90598
FieldFrom #1210To #1825
mathlib.declGaloisFieldFiniteField.instIsCyclicAlgEquivOfFinite
mathlib.moduleMathlib.FieldTheory.Finite.GaloisFieldMathlib.FieldTheory.Finite.Basic
noteMathlib's `GaloisField` and Frobenius theory cover the structure but no single 'Gal = ⟨Frob⟩' decl was found.`FiniteField.instIsCyclicAlgEquivOfFinite` proves the Galois group is cyclic; no single 'Gal = ⟨Frob⟩' decl was found.
modifiedCartesian product of sets73324a9e370c
FieldFrom #1210To #1825
mathlib.moduleMathlib.Data.Set.ProdMathlib.Data.Set.Operations
modifiedn th power of a setd8d72d0faa80
FieldFrom #1210To #1825
mathlib.moduleMathlib.Data.Set.ProdMathlib.Data.Set.Operations
modifiedSet of functions notation S^Tf04130b2e79b
FieldFrom #1210To #1825
mathlib.declPiCardinal.power_def
mathlib.match_kindexactinvocation
mathlib.moduleMathlib.Init.Data.PiMathlib.SetTheory.Cardinal.Defs
noteMathlib uses `T → S` (the Pi type) for function sets; cardinal exponentiation `#S ^ #T` matches by `Cardinal.power_def`.Mathlib uses `T → S` (the Pi type) for function sets; cardinal exponentiation `#S ^ #T` matches via `Cardinal.power_def`.
modifiedCanonical isomorphisms (currying)89f1b147c81e
FieldFrom #1210To #1825
mathlib.moduleMathlib.Logic.Equiv.BasicMathlib.Logic.Equiv.Prod
modifiedPower set as 2^Sae8144f3eaf6
FieldFrom #1210To #1825
mathlib.moduleMathlib.Data.Set.BasicMathlib.Data.Set.Defs
modifiedExponentiation as right adjoint to product6e223ae980ee
FieldFrom #1210To #1825
mathlib.moduleMathlib.CategoryTheory.Closed.CartesianMathlib.CategoryTheory.Monoidal.Closed.Cartesian
modifiedCartesian closed categoryab285dea869e
FieldFrom #1210To #1825
mathlib.moduleMathlib.CategoryTheory.Closed.CartesianMathlib.CategoryTheory.Monoidal.Closed.Cartesian
modifiedFunction compositione40a1132197c
FieldFrom #1210To #1825
mathlib.moduleMathlib.Init.FunctionInit.Prelude
modifiedn th iterate of a function88b65ca95d59
FieldFrom #1210To #1825
mathlib.declFunction.iterateNat.iterate
note`Function.iterate f n` is the nth iterate `f^[n]`.`Nat.iterate f n` is the nth iterate `f^[n]` (with `Function.iterate_*` API).
addedExponentiation by squaring0f0eb14b1a9e
addedRight-associativity of serial exponentiation28b8f55cee7d
addedSpecial limit defining e^x8040f8b4d96a
addedPolar form product rule0e9ec53af12a
addedCyclic group of order n from element of order n7aa803a2c9f6
addedNumber of primitive elements is φ(q-1)fb11ad420380
addedCurrying isomorphism for direct sums vs products14e34a87d4be