Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finite_field.pow_card_sub_one_eq_one

Modification history

2020-08-29 17:36
src/field_theory/finite.lean
feat(linear_algebra/char_poly/coeff,*): prerequisites for friendship theorem (#3953) …
Modified finite_field.pow_card_sub_one_eq_oneView on Github →
2020-05-17 20:01
src/field_theory/finite.lean
refactor(field_theory): preparations for Chevalley–Warning (#2590) …
Modified finite_field.pow_card_sub_one_eq_oneView on Github →
2020-05-05 19:08
src/field_theory/finite.lean
chore(field_theory/finite): meaningful variable names (#2606)
Modified finite_field.pow_card_sub_one_eq_oneView on Github →
2020-04-08 17:46
src/field_theory/finite.lean
feat(tactic/linter): add decidable_classical linter (#2352) …
Modified finite_field.pow_card_sub_one_eq_oneView on Github →
2020-03-05 13:17
src/field_theory/finite.lean
chore(*): switch to lean 3.6.1 (#2064) …
Modified finite_field.pow_card_sub_one_eq_oneView on Github →
2019-03-05 09:21
src/field_theory/finite.lean
feat(linear_algebra): module (vector space) structure for finsupp, matrix, and mv polynomials
Added finite_field.pow_card_sub_one_eq_oneView on Github →