Def RatFunc.coePolynomial

Modification history

2024-04-22 02:25

Mathlib/FieldTheory/RatFunc.lean

feat (Mathlib/FieldTheory/RatFunc.lean): add five lemmas about coercions between Hahn or Laurent Series and Rational Functions (#12245) …

Added RatFunc.coePolynomial View on Github →