Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 13:28 745099b8

View on Github →

chore(*/parity): Generalize lemmas and clarify names (#13268) Generalizations

Estimated changes

Modified src/algebra/geom_sum.lean

Modified src/algebra/group_power/basic.lean

added theorem neg_one_sq

modified theorem neg_sq

Modified src/algebra/order/sub.lean

added theorem tsub_add_tsub_comm

Modified src/algebra/parity.lean

added theorem even.neg_one_pow

added theorem even.neg_one_zpow

added theorem even.neg_pow

added theorem even.neg_zpow

modified theorem even.sub_odd

added theorem even.tsub_even

deleted theorem even.zpow_neg

deleted theorem even.zpow_nonneg

added theorem even_iff_exists_bit0

modified theorem is_square.map

modified theorem is_square_sq

modified theorem odd.neg

added theorem odd.neg_one_pow

added theorem odd.neg_one_zpow

added theorem odd.neg_pow

added theorem odd.neg_zpow

modified theorem odd.sub_even

modified theorem odd.sub_odd

deleted theorem odd.zpow_nonneg

modified theorem odd_bit1

added theorem odd_iff_exists_bit1

Modified src/analysis/convex/specific_functions.lean

Modified src/data/int/parity.lean

Modified src/data/nat/digits.lean

Modified src/data/nat/parity.lean

deleted theorem nat.even.sub_even

deleted theorem nat.neg_one_pow_eq_one_iff_even

deleted theorem nat.neg_one_pow_of_even

deleted theorem nat.neg_one_pow_of_odd

deleted theorem nat.neg_one_sq

added theorem neg_one_pow_eq_one_iff_even

Modified src/group_theory/specific_groups/alternating.lean

Modified src/linear_algebra/general_linear_group.lean

Modified src/linear_algebra/special_linear_group.lean

Modified src/number_theory/bernoulli.lean

Modified src/number_theory/cyclotomic/discriminant.lean

Modified src/number_theory/cyclotomic/primitive_roots.lean