Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.of_real_eval

Modification history

2023-01-24 03:14
src/data/is_R_or_C/basic.lean
refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade imports (#18217) …
Modified polynomial.of_real_evalView on Github →
2022-04-11 11:52
src/data/complex/is_R_or_C.lean
feat(data/complex/is_R_or_C): add `polynomial.of_real_eval` (#13287)
Added polynomial.of_real_evalView on Github →