English
There is a canonical representation of RatFunc given by RatFunc.mk p q when q ≠ 0, matching the fraction built from p and q after localization.
Русский
Существует каноническая репрезентация RatFunc как RatFunc.mk p q при q ≠ 0, совпадающая с дробью p/q после локализации.
LaTeX
$$$\\text{RatFunc.mk}\\, p\\, q = \\text{ofFractionRing}(\\text{Localization.mk}'(p,q))$$$
Lean4
/-- `RatFunc.mk (p q : K[X])` is `p / q` as a rational function.
If `q = 0`, then `mk` returns 0.
This is an auxiliary definition used to define an `Algebra` structure on `RatFunc`;
the `simp` normal form of `mk p q` is `algebraMap _ _ p / algebraMap _ _ q`.
-/
def mk :=
val_proj @wrapped✝.{}
