Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finite_field.exists_root_sum_quadratic

Modification history

2022-02-08 12:43
src/field_theory/finite/basic.lean
feat(*): localized `R[X]` notation for `polynomial R` (#11895) …
Modified finite_field.exists_root_sum_quadraticView on Github →
2020-05-17 20:01
src/field_theory/finite.lean
refactor(field_theory): preparations for Chevalley–Warning (#2590) …
Modified finite_field.exists_root_sum_quadraticView on Github →
2020-05-05 19:08
src/field_theory/finite.lean
chore(field_theory/finite): meaningful variable names (#2606)
Modified finite_field.exists_root_sum_quadraticView on Github →
2019-10-16 17:05
src/field_theory/finite.lean
feat(field_theory/finite): cardinality of images of polynomials (#1554) …
Added finite_field.exists_root_sum_quadraticView on Github →