Theorems · Inductive type · field theory

RatFunc

(K : Type u) → [CommRing K] → Type u

RatFunc K is K(X), the field of rational functions over K. The inclusion of polynomials into RatFunc is algebraMap K[X] K⟮X⟯, the maps between K⟮X⟯ and another field of fractions of K[X], especially FractionRing K[X], are given by IsLocalization.algEquiv.

Defined in

Mathlib.FieldTheory.RatFunc.Defs

Cited by

301 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CommRing