From 8cebe691a2866398f0fc34409ee31beb2f9c93ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Tue, 7 Oct 2025 08:57:46 -0400 Subject: [PATCH] fix: `Nat.and_distrib_right` -> `Nat.and_or_distrib_right` (#10649) This PR renames `Nat.and_distrib_right` to `Nat.and_or_distrib_right`. This is to make the name consistent with other theorems in the same file (e.g. `Nat.and_or_distrib_left`). --- src/Init/Data/Nat/Bitwise/Lemmas.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index 09e1c0813e..96be0f6235 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -591,10 +591,13 @@ theorem and_or_distrib_left (x y z : Nat) : x &&& (y ||| z) = (x &&& y) ||| (x & simp [Bool.and_or_distrib_left] @[grind =] -theorem and_distrib_right (x y z : Nat) : (x ||| y) &&& z = (x &&& z) ||| (y &&& z) := by +theorem and_or_distrib_right (x y z : Nat) : (x ||| y) &&& z = (x &&& z) ||| (y &&& z) := by apply Nat.eq_of_testBit_eq simp [Bool.and_or_distrib_right] +@[deprecated and_or_distrib_right (since := "2025-10-02")] +abbrev and_distrib_right := and_or_distrib_right + theorem or_and_distrib_left (x y z : Nat) : x ||| (y &&& z) = (x ||| y) &&& (x ||| z) := by apply Nat.eq_of_testBit_eq simp [Bool.or_and_distrib_left]