@[reducible, inline]

abbrev MvRatFunc (σ : Type u_1) (K : Type u_2) [CommRing K] : Type (max u_2 u_1)

The field of multivariate rational functions in variables indexed by σ over a commutative ring K, defined as the fraction field of the multivariate polynomial ring MvPolynomial σ K.

Equations

• MvRatFunc σ K = FractionRing (MvPolynomial σ K)

def IsDefined (σ : Type u_1) (K : Type u_2) [CommRing K] [IsDomain K] (g : MvRatFunc σ K) (x₀ : σ → K) : Prop

A rational function $g$ is defined at a point $x_0$ if $g$ can be written as $p / q$ where $p, q$ are polynomials and $q(x_0) \neq 0$.

Equations

• One or more equations did not get rendered due to their size.