Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 10:08 37c0d539

View on Github →

refactor(field_theory/finite): generalize proofs (#429)

Estimated changes

Modified data/equiv/algebra.lean

added theorem equiv.coe_units_equiv_ne_zero

added def equiv.units_equiv_ne_zero

Modified data/nat/gcd.lean

added theorem nat.gcd_gcd_self_left_left

added theorem nat.gcd_gcd_self_left_right

added theorem nat.gcd_gcd_self_right_left

added theorem nat.gcd_gcd_self_right_right

added theorem nat.gcd_mul_left_left

added theorem nat.gcd_mul_left_right

added theorem nat.gcd_mul_right_left

added theorem nat.gcd_mul_right_right

Modified data/zmod/quadratic_reciprocity.lean

Modified field_theory/finite.lean

added theorem card_nth_roots_subgroup_units

deleted theorem coe_units_equiv_ne_zero

deleted theorem finite_field.card_nth_roots_units

deleted theorem finite_field.card_order_of_eq_totient

deleted theorem finite_field.card_pow_eq_one_eq_order_of

modified theorem finite_field.card_units

modified theorem finite_field.prod_univ_units_id_eq_neg_one

deleted theorem order_of_pow

deleted def units_equiv_ne_zero

Modified group_theory/order_of_element.lean

added theorem card_order_of_eq_totient_aux₂

added theorem card_pow_eq_one_eq_order_of_aux

added theorem is_cyclic.card_order_of_eq_totient

added theorem is_cyclic.card_pow_eq_one_le

added def is_cyclic.comm_group

added theorem is_cyclic_of_card_pow_eq_one_le

added theorem order_of_eq_card_of_forall_mem_gpowers

deleted theorem order_of_eq_card_of_forall_mem_gppowers

added theorem order_of_pow

added theorem pow_gcd_card_eq_one_iff