Commit 2024-08-12 19:34 1c910395

View on Github →

perf(CharP/CharZero): scope simp theorems with weak keys (#15631) These have keys like HAdd.hAdd _ _ _ _ _ _ but are specific to characteristic two and zero.

Estimated changes

Modified Mathlib/Algebra/CharP/Two.lean

Modified Mathlib/Algebra/CharZero/Lemmas.lean

added theorem CharZero.eq_neg_self_iff

added theorem CharZero.neg_eq_self_iff

deleted theorem eq_neg_self_iff

deleted theorem neg_eq_self_iff

Modified Mathlib/Analysis/Complex/Isometry.lean

Modified Mathlib/Geometry/Euclidean/Triangle.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean

Modified Mathlib/NumberTheory/LSeries/RiemannZeta.lean

Modified Mathlib/NumberTheory/LegendreSymbol/Basic.lean

Modified Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean

Modified Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean

Modified Mathlib/NumberTheory/Pell.lean