Commit 2023-08-14 19:43 704efa4d

View on Github →

feat: lemmas about parity and Nat.antidiagonal (#6540)

Estimated changes

Modified Mathlib/Algebra/GroupPower/Ring.lean

Modified Mathlib/Algebra/Parity.lean

added theorem Even.add_one

added theorem Even.odd_add

added theorem Even.one_add

added theorem odd_add_one_self'

added theorem odd_add_one_self

added theorem odd_add_self_one'

added theorem one_add_self_self

Modified Mathlib/Data/Finset/NatAntidiagonal.lean

added theorem Finset.Nat.antidiagonal_filter_fst_le_of_le

added theorem Finset.Nat.antidiagonal_filter_le_fst_of_le

added theorem Finset.Nat.antidiagonal_filter_le_snd_of_le

added theorem Finset.Nat.antidiagonal_filter_snd_le_of_le

added theorem Finset.Nat.map_prodComm_antidiagonal

modified theorem Finset.Nat.map_swap_antidiagonal

Modified Mathlib/NumberTheory/Cyclotomic/Discriminant.lean