Commit 2021-03-24 05:49 935003eb

View on Github →

chore(data/nat/basic): add @[simp] to some lemmas about numerals (#6652) Allows the simplifier to make more progress in equalities of numerals (both in nat, and in [(semi)ring R] [no_zero_divisors R] [char_zero R]). Also adds @[simp] to nat.succ_ne_zero and nat.succ_ne_self.

Estimated changes

Modified src/algebra/char_zero.lean

added theorem bit0_eq_bit0

added theorem bit0_injective

added theorem bit1_eq_bit1

added theorem bit1_eq_one

added theorem bit1_injective

added theorem nat_mul_inj'

added theorem nat_mul_inj

added theorem one_eq_bit1

added theorem zero_eq_bit0

Modified src/analysis/normed_space/operator_norm.lean

Modified src/data/nat/basic.lean

added theorem nat.bit0_eq_bit0

added theorem nat.bit1_eq_bit1

added theorem nat.bit1_eq_one

added theorem nat.one_eq_bit1

Modified src/data/sym2.lean

Modified src/ring_theory/polynomial/bernstein.lean