Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-05 12:48 4b4975cf

View on Github →

feat(<various>): add a bunch of lemmas for use with Jacobi symbols (#16290) This PR introduces a number of lemmas that will be needed for proving results about the Jacobi symbol (to be introduced in a follow-up PR). (Originally, the Jacobi symbol results were included here; see the discussion below.) Discussion on Zuilp.

Estimated changes

Modified src/data/list/basic.lean

added theorem list.pmap_append'

added theorem list.pmap_append

Modified src/data/nat/factorization/basic.lean

added theorem nat.exists_eq_pow_mul_and_not_dvd

Modified src/data/nat/parity.lean

added theorem even.mod_even

added theorem even.mod_even_iff

added theorem odd.factors_ne_two

added theorem odd.mod_even

added theorem odd.mod_even_iff

Modified src/data/sign.lean

added theorem sign_type.range_eq

Created src/data/zmod/coprime.lean

added theorem zmod.eq_zero_iff_gcd_ne_one

added theorem zmod.eq_zero_of_gcd_ne_one

added theorem zmod.ne_zero_of_gcd_eq_one

Modified src/number_theory/legendre_symbol/zmod_char.lean

added theorem zmod.χ₄_int_mod_four

added theorem zmod.χ₄_int_one_mod_four

added theorem zmod.χ₄_int_three_mod_four

added theorem zmod.χ₄_nat_mod_four

added theorem zmod.χ₄_nat_one_mod_four

added theorem zmod.χ₄_nat_three_mod_four

added theorem zmod.χ₈_int_mod_eight

added theorem zmod.χ₈_nat_mod_eight

Modified src/ring_theory/int/basic.lean

added theorem int.gcd_eq_one_of_gcd_mul_right_eq_one_left

added theorem int.gcd_eq_one_of_gcd_mul_right_eq_one_right

added theorem int.gcd_ne_one_iff_gcd_mul_right_ne_one