Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-25 14:53 5deb96d5

View on Github →

feat(data/mv_polynomial/funext): function extensionality for polynomials (#4196) over infinite integral domains

Estimated changes

added theorem ring_equiv.trans_apply
modified theorem mv_polynomial.C_inj
modified theorem mv_polynomial.C_injective
added theorem mv_polynomial.funext
added theorem polynomial.funext
added def function.extend
added theorem function.extend_apply
added theorem function.extend_comp
added theorem function.extend_def