Commit 2024-04-22 02:25 073c0142

View on Github →

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

Estimated changes

Modified Mathlib/FieldTheory/RatFunc.lean

added def RatFunc.coePolynomial

added theorem RatFunc.coe_coe

added theorem RatFunc.coe_ne_zero

added theorem RatFunc.single_inv

added theorem RatFunc.single_one_eq_pow

added theorem RatFunc.single_zpow