Mathlib Changelog
v3
Changelog
About
Github
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