Mathlib v3 is deprecated. Go to Mathlib v4

Theorem card_nth_roots_subgroup_units

Modification history

2022-08-17 14:53
src/ring_theory/integral_domain.lean
chore(group_theory/*): Fix lint (#16095) …
Modified card_nth_roots_subgroup_unitsView on Github →
2020-05-17 20:01
src/ring_theory/integral_domain.lean
refactor(field_theory): preparations for Chevalley–Warning (#2590) …
Modified card_nth_roots_subgroup_unitsView on Github →
2020-05-12 06:37
src/field_theory/finite.lean
feat(ring_theory/integral_domain): sum in integral domain indexed by finite group (#2623) …
Modified card_nth_roots_subgroup_unitsView on Github →
2020-05-05 19:08
src/field_theory/finite.lean
chore(field_theory/finite): meaningful variable names (#2606)
Modified card_nth_roots_subgroup_unitsView on Github →
2020-04-08 17:46
src/field_theory/finite.lean
feat(tactic/linter): add decidable_classical linter (#2352) …
Modified card_nth_roots_subgroup_unitsView on Github →
2018-11-05 10:08
field_theory/finite.lean
refactor(field_theory/finite): generalize proofs (#429)
Added card_nth_roots_subgroup_unitsView on Github →