Commit 2024-01-26 07:29 0500719e

View on Github →

feat: Int.{even_sub_one,even_mul_pred_self} (#9859) Also rename Nat.even_mul_self_pred for consistency with Nat.even_mul_succ_self.

Estimated changes

Modified Mathlib/Algebra/GroupPower/NegOnePow.lean

Modified Mathlib/Data/Int/Parity.lean

added theorem Int.even_mul_pred_self

added theorem Int.even_sub_one

Modified Mathlib/Data/Nat/Parity.lean

added theorem Nat.even_mul_pred_self

deleted theorem Nat.even_mul_self_pred

Modified Mathlib/RingTheory/Discriminant.lean