Theorems · Definition · field theory

RatFunc.mk

{K : Type u_1} → [inst : CommRing K] → [IsDomain K] → Polynomial K → Polynomial K → RatFunc K

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.

Defined in

Mathlib.FieldTheory.RatFunc.Defs

Cited by

21 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomain