Revision #3175 → #3703 · back to history
modifiedExponentiation (positive integer exponent)b8fc6a52cb1b
| Field | From #3175 | To #3703 |
|---|
| mathlib.module | Mathlib.Algebra.Group.Defs | Mathlib.Algebra.Group.Monoid |
| note | `Monoid.npow` is the canonical inductive definition of iterated multiplication on a monoid. | `Monoid.npow` is the class field defining iterated multiplication on a monoid. |
modifiedZeroth, negative, and fractional powers649819e3e1bf
| Field | From #3175 | To #3703 |
|---|
| note | Integer powers via `zpowRec`/`DivInvMonoid.zpow`, and rational/real extensions via `Real.rpow`. | `zpowRec`/`DivInvMonoid.zpow` cover integer powers and `Real.rpow` real ones. |
modifiedArchimedes' law of exponents for powers of tencae51c3b8666
| Field | From #3175 | To #3703 |
|---|
| note | Mathlib has the general `pow_add` law; the Archimedes historical specialization to powers of ten is not stated separately. | The generic `pow_add` law subsumes the historical powers-of-ten specialization. |
modifiedCube of b09ec9b6ab322
| Field | From #3175 | To #3703 |
|---|
| note | There is no dedicated `cube` decl; one uses `a^3` directly. | No dedicated `cube` decl; users write `a^3`. |
modifiedInductive definition of positive integer exponentiation65bede8935e2
| Field | From #3175 | To #3703 |
|---|
| mathlib.module | Mathlib.Algebra.Group.Defs | Mathlib.Algebra.Group.Monoid |
| note | `Monoid.npow_zero` and `Monoid.npow_succ` provide the inductive base and step. | `Monoid.npow_zero`/`Monoid.npow_succ` (class fields) give the inductive base/step. |
modifiedZero to the power of zero822eb083404a
| Field | From #3175 | To #3703 |
|---|
| note | Mathlib follows the convention `0^0 = 1` via `pow_zero`. | Mathlib adopts the convention `0^0 = 1` via `pow_zero`. |
modifiedNegative exponents in a monoid2a6bf781248e
| Field | From #3175 | To #3703 |
|---|
| mathlib.decl | ZPow.zpow | DivInvMonoid.zpow |
| mathlib.module | Mathlib.Algebra.Group.Defs | Mathlib.Algebra.Group.DivInvMonoid |
| note | `DivInvMonoid.zpow` defines integer powers for invertible elements. | `DivInvMonoid.zpow` (class field) defines integer powers for invertible elements. |
modifiedAlternating sign of powers of -1d0fd6a7cd129
| Field | From #3175 | To #3703 |
|---|
| note | `neg_one_pow_eq_pow_mod_two` captures the alternation; related `Odd.neg_one_pow` etc. | `neg_one_pow_eq_pow_mod_two` captures the alternation. |
modifiedPowers of negative bases do not converge0dcae5e47f31
| Field | From #3175 | To #3703 |
|---|
| note | No dedicated non-convergence lemma for `b<-1` in Mathlib. | No dedicated non-convergence lemma for `b<-1`. |
modifiedPower functions3c4827f1b026
| Field | From #3175 | To #3703 |
|---|
| note | The terminology `power function` has no dedicated Mathlib decl. | No dedicated `power function` decl. |
modifiedEven and odd power functions89bd5c3f059d
| Field | From #3175 | To #3703 |
|---|
| note | No `evenPowerFunction`/`oddPowerFunction` family is defined. | No `evenPowerFunction`/`oddPowerFunction` family. |
modifiedn th root of a nonnegative real7e1cc4582dfe
| Field | From #3175 | To #3703 |
|---|
| note | Nth roots are realized as `x ^ (1/n : ℝ)` using `Real.rpow`. | Nth roots are realized as `x ^ (1/n : ℝ)` via `Real.rpow`. |
modifiedPrincipal value and multivaluedness for negative bases2dd8e4958762
| Field | From #3175 | To #3703 |
|---|
| note | `Real.rpow_def_of_neg` gives a specific principal-value formula for `x < 0` but does not develop the multivalued discussion. | `Real.rpow_def_of_neg` gives a principal-value formula for `x < 0` but no multivalued discussion. |
modifiedReal exponent via limit of rational exponents4b6e5be81529
| Field | From #3175 | To #3703 |
|---|
| note | Mathlib defines `Real.rpow` via `exp ∘ log` rather than as a limit of rational approximations, though continuity is proved. | Mathlib uses `exp ∘ log` rather than the rational-limit construction, though continuity is proved. |
modifiedExponential function (limit definition)c1eb40e25a6c
| Field | From #3175 | To #3703 |
|---|
| note | `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`. | `Real.exp` uses the power series; the `(1+x/n)^n` limit form is proved equivalent via `Real.tendsto_one_add_div_pow_exp`. |
modifiedEuler's numberc7fea11fa08c
| Field | From #3175 | To #3703 |
|---|
| note | Mathlib has no dedicated `Real.e` constant; Euler's number is `Real.exp 1`, with numerical bounds like `Real.exp_one_gt_two`. | No dedicated `Real.e`; Euler's number is `Real.exp 1` with numerical bounds like `Real.exp_one_gt_two`. |
modifiedPolar form of n th roots of a complex number83e88beba778
| Field | From #3175 | To #3703 |
|---|
| note | Mathlib has nth-root theory and `Complex.cpow` but no single decl in polar form. | Mathlib has nth-root theory and `Complex.cpow`, but no polar-form decl. |
modifiedn distinct n th roots of a complex numberf278491112b6
| Field | From #3175 | To #3703 |
|---|
| note | `IsPrimitiveRoot.card_nthRoots` gives that `nthRoots n a` has cardinality `n` (when a root exists). | `IsPrimitiveRoot.card_nthRoots` gives that `nthRoots n a` has cardinality `n`. |
modifiedPrincipal n th root29b0f5b00a47
| Field | From #3175 | To #3703 |
|---|
| note | Principal root is `z ^ (1/n : ℂ)` via `Complex.cpow`; no `principalNthRoot` decl. | Principal root is `z ^ (1/n : ℂ)` via `Complex.cpow`; no dedicated `principalNthRoot`. |
modifiedNo continuous n th root on all of Ca8e38b259330
| Field | From #3175 | To #3703 |
|---|
| note | No dedicated obstruction lemma; related discontinuity of `Complex.log` at 0 is known. | No dedicated obstruction lemma. |
modifiedn th roots via roots of unity27bdda34c05a
| Field | From #3175 | To #3703 |
|---|
| note | Mathlib relates nth roots to primitive roots, e.g. via `IsPrimitiveRoot.nthRoots_eq`. | Mathlib relates nth roots to primitive roots via `IsPrimitiveRoot.nthRoots_eq`. |
modifiedGeometric arrangement of roots of unityc7711f9e9334
| Field | From #3175 | To #3703 |
|---|
| note | Roots of unity arise as `exp (2π i k / n)` via `Complex.isPrimitiveRoot_exp`; no specific 'regular polygon' lemma. | Roots of unity arise as `exp (2π i k / n)`; no explicit 'regular polygon' lemma. |
modifiedOther values of multivalued logarithm and exponentiation93a7085406d1
| Field | From #3175 | To #3703 |
|---|
| note | Mathlib uses principal values; no multivalued branch enumeration. Anchor tightened to disambiguate from other 'If' sentences in this section. | Mathlib uses principal values; no multivalued branch enumeration. |
modifiedNumber of values of z^w for rational wa13de209f360
| Field | From #3175 | To #3703 |
|---|
| note | No multivalued count lemma in Mathlib. Anchor tightened to disambiguate from other 'If' sentences in this section. | No multivalued-count lemma in Mathlib. |
modifiedAlgebraic base, rational exponent gives algebraic131a33a7d52a
| Field | From #3175 | To #3703 |
|---|
| note | `IsAlgebraic.pow` covers integer powers; the rational exponent case via nth roots is not given a single Mathlib lemma. | `IsAlgebraic.pow` covers integer powers; the rational-exponent case via nth roots has no single lemma. |
modifiedExponentiation in a monoid63e93d132c8f
| Field | From #3175 | To #3703 |
|---|
| mathlib.module | Mathlib.Algebra.Group.Defs | Mathlib.Algebra.Group.Monoid |
| note | `Monoid.npow` is monoid exponentiation. | `Monoid.npow` (class field) is monoid exponentiation. |
modifiedNegative integer exponent in a monoided7436404a32
| Field | From #3175 | To #3703 |
|---|
| mathlib.decl | ZPow.zpow | DivInvMonoid.zpow |
| mathlib.module | Mathlib.Algebra.Group.Defs | Mathlib.Algebra.Group.DivInvMonoid |
| note | `DivInvMonoid.zpow` extends to negative integer exponents. | `DivInvMonoid.zpow` (class field) extends to negative integer exponents. |
modifiedConjugation notation0b9804e7e594
| Field | From #3175 | To #3703 |
|---|
| note | Mathlib has `conj_pow` (and `Units.conj_pow`) but no `x^y` conjugation notation per se. | Mathlib has `conj_pow` but no `x^y` conjugation notation. |
modifiedMatrix power7ea7c89cd85c
| Field | From #3175 | To #3703 |
|---|
| mathlib.module | Mathlib.Algebra.Group.Defs | Mathlib.Algebra.Group.Monoid |
| note | Square matrices form a monoid, so `A^n` is given by `Monoid.npow`; many `Matrix.*_pow` lemmas exist. | Square matrices are a monoid, so `A^n` is `Monoid.npow`; many `Matrix.*_pow` lemmas exist. |
modifiedFinite field1c7b933b7c9d
| Field | From #3175 | To #3703 |
|---|
| note | Finite fields are realised as `Field` with `Finite`; `GaloisField p n` is the canonical construction. | `GaloisField p n` is the canonical finite field construction. |
modifiedPrimitive element of a finite fieldebe7f86da493
| Field | From #3175 | To #3703 |
|---|
| note | `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. | `instIsCyclicUnitsOfFinite` gives cyclicity of the unit group, so a primitive element exists; no dedicated decl. |
modifiedGalois group of finite field extensionda5709b90598
| Field | From #3175 | To #3703 |
|---|
| note | `FiniteField.instIsCyclicAlgEquivOfFinite` proves the Galois group is cyclic; no single 'Gal = ⟨Frob⟩' decl was found. | `FiniteField.instIsCyclicAlgEquivOfFinite` proves the Galois group is cyclic; no single 'Gal = ⟨Frob⟩' decl. |
modifiedn th power of a setd8d72d0faa80
| Field | From #3175 | To #3703 |
|---|
| note | Iterated Cartesian power is realised via `Fin n → S` or `Set.pi`, but there is no `Set.npow` decl. | Iterated Cartesian power is realised via `Fin n → S` or `Set.pi`; no `Set.npow` decl. |
modifiedSet of functions notation S^Tf04130b2e79b
| Field | From #3175 | To #3703 |
|---|
| note | Mathlib uses `T → S` (the Pi type) for function sets; cardinal exponentiation `#S ^ #T` matches via `Cardinal.power_def`. | Mathlib uses the Pi type `T → S`; cardinal exponentiation matches via `Cardinal.power_def`. |
modifiedPower set as 2^Sae8144f3eaf6
| Field | From #3175 | To #3703 |
|---|
| note | `Set.powerset` and `Finset.powerset` realise `2^S`; cardinality via `Fintype.card_finset`. | `Set.powerset` and `Finset.powerset` realise `2^S`. |
modifiedExponentiation as right adjoint to product6e223ae980ee
| Field | From #3175 | To #3703 |
|---|
| note | `CategoryTheory.ihom.adjunction` gives the `tensorLeft A ⊣ ihom A` adjunction, which specialises to the product ⊣ exp adjunction in a cartesian monoidal category. | `CategoryTheory.ihom.adjunction` gives the `tensorLeft A ⊣ ihom A` adjunction that specialises to product ⊣ exp. |
modifiedCartesian closed categoryab285dea869e
| Field | From #3175 | To #3703 |
|---|
| note | The dedicated `CartesianClosed` class was deprecated; cartesian closed categories are now `MonoidalClosed C` with `[CartesianMonoidalCategory C]`. | Cartesian closed categories are realised as `MonoidalClosed C` with `[CartesianMonoidalCategory C]`. |
modifiedTetration and hyperoperation6f5e23b65631
| Field | From #3175 | To #3703 |
|---|
| note | `hyperoperation` defines the hyperoperation hierarchy with tetration at level 4. | `hyperoperation` defines the hierarchy with tetration at level 4. |
modifiedHyperoperation evaluated at (3,3)980feef191b5
| Field | From #3175 | To #3703 |
|---|
| note | Specific numerical evaluation example; not a Mathlib lemma. | Specific numerical evaluation; not a Mathlib lemma. |
modifiedn th iterate of a function88b65ca95d59
| Field | From #3175 | To #3703 |
|---|
| note | `Nat.iterate f n` is the nth iterate `f^[n]` (with `Function.iterate_*` API). | `Nat.iterate f n` is the nth iterate `f^[n]`. |
modifiedInverse function notation f^{-1}60a8795030a0
| Field | From #3175 | To #3703 |
|---|
| note | `Function.invFun` / `Equiv.symm` formalise the inverse-function notation. | `Function.invFun` / `Equiv.symm` formalise inverse-function notation. |
modifiedExponentiation by squaring0f0eb14b1a9e
| Field | From #3175 | To #3703 |
|---|
| note | `npowBinRec` is Mathlib's repeated-squaring implementation of `npow`, equated to `npowRec` via `npowRec_eq_npowBinRec`. | `npowBinRec` is Mathlib's repeated-squaring implementation, equated to `npowRec` via `npowRec_eq_npowBinRec`. |
modifiedSpecial limit defining e^x8040f8b4d96a
| Field | From #3175 | To #3703 |
|---|
| note | `Real.tendsto_one_add_div_pow_exp` proves `(1 + t/n)^n → exp t` as `n → ∞`. | `Real.tendsto_one_add_div_pow_exp` proves `(1 + t/n)^n → exp t`. |
modifiedPolar form product rule0e9ec53af12a
| Field | From #3175 | To #3703 |
|---|
| note | `Complex.arg_mul` and multiplicativity of `Complex.abs` give the polar product rule. | `Complex.arg_mul` plus multiplicativity of `Complex.abs` give the polar product rule. |
modifiedCyclic group of order n from element of order n7aa803a2c9f6
| Field | From #3175 | To #3703 |
|---|
| note | Mathlib relates `orderOf x = n` to the finite cyclic subgroup `Subgroup.zpowers x` via `orderOf_eq_card_of_zpowers_eq_top`. | Mathlib relates `orderOf x = n` to the cyclic subgroup `Subgroup.zpowers x`. |
modifiedNumber of primitive elements is φ(q-1)fb11ad420380
| Field | From #3175 | To #3703 |
|---|
| note | Count of generators of a cyclic group of order n is `Nat.totient n`; specialization to finite fields is via cyclicity of the unit group. | Count of generators of a cyclic group of order n is `Nat.totient n`; no direct 'φ(q-1) primitives' decl. |
addedFermat's little theorem for finite fields43da0459209d
addedNumber of primitive n-th roots of unity is φ(n)40f846f30c35
addedRadical of an ideal is a radical ideal7edc2a7c36a6