Commit 2023-11-30 22:26 89670c59

View on Github →

feat: add a few simp lemmas (#8750)

Remove simp-lemma bitwise_of_ne_zero, since it wasn't used, and could cause loops in an inconsistent context.

Estimated changes

Modified Mathlib/Algebra/CharZero/Lemmas.lean

modified theorem eq_neg_self_iff

modified theorem neg_eq_self_iff

Modified Mathlib/Algebra/GroupPower/Ring.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Data/Int/ModEq.lean

Modified Mathlib/Data/Int/Order/Units.lean

modified theorem Int.neg_one_pow_ne_zero

Modified Mathlib/Data/Nat/Bitwise.lean

Modified Mathlib/Geometry/Euclidean/Triangle.lean

Modified Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

Modified Mathlib/RingTheory/WittVector/Frobenius.lean

Modified Mathlib/Topology/MetricSpace/PiNat.lean