mathlib3

fadbd959 - feat(field_theory/ratfunc): ratfunc.lift_on without is_domain (#11227)

feat(field_theory/ratfunc): ratfunc.lift_on without is_domain (#11227) We might want to state results about rational functions without assuming that the base ring is an integral domain. Cf. Misconceptions about $K_X$, Kleiman, Steven; Stacks01X1 Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>