Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.exists_coeff_not_mem_C_inverse

Modification history

2022-08-09 17:00
src/data/polynomial/induction.lean
chore(data/polynomial/induction): cleanup (#15918) …
Deleted polynomial.exists_coeff_not_mem_C_inverseView on Github →
2021-05-07 09:30
src/data/polynomial/coeff.lean
refactor(polynomial/*): make polynomials irreducible (#7421) …
Modified polynomial.exists_coeff_not_mem_C_inverseView on Github →
2021-01-20 09:51
src/data/polynomial/coeff.lean
feat(algebraic_geometry/is_open_comap_C): add file is_open_comap_C, prove that Spec R[x] \to Spec R is an open map (#5693) …
Added polynomial.exists_coeff_not_mem_C_inverseView on Github →