Elementary functions (trigonometric, rational, \(\exp\), \(\log\), etc)

DefinitionPolynomial functions#

eval x p is the evaluation of the polynomial p at x

Polynomial.eval.{u} {R : Type u} [Semiring R] (x : R) (p : Polynomial R) : R
Sources
MathlibPolynomial.eval
Uses 2 · Used by 10
Statement usesPolynomial in one indeterminate · Ring morphism
Used byThe Factor and Remainder Theorems · \(\C\) is algebraically closed · Multiplicity · Roots of a polynomial · Cayley-Hamilton theorem · Polynomial-time computation · Rational root theorem · Weierstrass polynomial approximation theorem · Taylor's theorem with integral form for remainder (Taylor-like theorems) · Taylor's theorem with Lagrange form for remainder

DefinitionRational functions#

Evaluate a rational function p given a ring hom f from the scalar field to the target and a value x for the variable in the target.

Fractions are reduced by clearing common denominators before evaluating: eval id 1 ((X^2 - 1) / (X - 1)) = eval id 1 (X + 1) = 2, not 0 / 0 = 0.

RatFunc.eval.{u} {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L)
  (p : RatFunc K) : L
Sources
MathlibRatFunc.eval
Uses 6
Statement usesField · Greatest common divisor · Least common multiple · Linear map · Rational fraction fields with one indeterminate over a field · Rational number

DefinitionPower functions#

The real power function x ^ y, defined as the real part of the complex power function. For x > 0, it is equal to exp (y log x). For x = 0, one sets 0 ^ 0=1 and 0 ^ y=0 for y ≠ 0. For x < 0, the definition is somewhat arbitrary as it depends on the choice of a complex determination of the logarithm. With our conventions, it is equal to exp (y log x) cos (π y).

Real.rpow (x y : ℝ) : ℝ
Sources
MathlibReal.rpow
Uses 1
Statement usesComplex number

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.