Commit 2023-06-05 05:13 496e831e

View on Github →

feat: port FieldTheory.Laurent (#4512)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Laurent.lean

added def RatFunc.laurent

added def RatFunc.laurentAux

added theorem RatFunc.laurentAux_algebraMap

added theorem RatFunc.laurentAux_div

added theorem RatFunc.laurentAux_ofFractionRing_mk

added theorem RatFunc.laurent_C

added theorem RatFunc.laurent_X

added theorem RatFunc.laurent_algebraMap

added theorem RatFunc.laurent_at_zero

added theorem RatFunc.laurent_div

added theorem RatFunc.laurent_injective

added theorem RatFunc.laurent_laurent

added theorem RatFunc.taylor_mem_nonZeroDivisors