From 416bfc2c1d41f08f9856c5dd00d5e1558aa80673 Mon Sep 17 00:00:00 2001 From: Pol_tta Date: Sat, 11 Mar 2023 14:23:55 +0000 Subject: [PATCH] fix: Fix aligns (#2781) --- Mathlib/Algebra/GroupWithZero/Defs.lean | 2 ++ Mathlib/Init/Data/Nat/Bitwise.lean | 6 +++--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/GroupWithZero/Defs.lean b/Mathlib/Algebra/GroupWithZero/Defs.lean index 2fe6bb21ac170..51e7537171234 100644 --- a/Mathlib/Algebra/GroupWithZero/Defs.lean +++ b/Mathlib/Algebra/GroupWithZero/Defs.lean @@ -99,6 +99,8 @@ class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] export MulZeroClass (zero_mul mul_zero) attribute [simp] zero_mul mul_zero +#align zero_mul MulZeroClass.zero_mul +#align mul_zero MulZeroClass.mul_zero /-- Predicate typeclass for expressing that `a * b = 0` implies `a = 0` or `b = 0` for all `a` and `b` of type `G₀`. -/ diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean index 2bc3e10665611..fbf7b0e25494b 100644 --- a/Mathlib/Init/Data/Nat/Bitwise.lean +++ b/Mathlib/Init/Data/Nat/Bitwise.lean @@ -283,17 +283,17 @@ def bits : ℕ → List Bool := def bitwise' (f : Bool → Bool → Bool) : ℕ → ℕ → ℕ := binaryRec (fun n => cond (f false true) n 0) fun a m Ia => binaryRec (cond (f true false) (bit a m) 0) fun b n _ => bit (f a b) (Ia n) -#align nat.bitwise Nat.bitwise +#align nat.bitwise Nat.bitwise' /--`lor'` takes two natural numbers and returns their bitwise `or`-/ def lor' : ℕ → ℕ → ℕ := bitwise' or -#align nat.lor Nat.lor +#align nat.lor Nat.lor' /--`land'` takes two naturals numbers and returns their `and`-/ def land' : ℕ → ℕ → ℕ := bitwise' and -#align nat.land Nat.land +#align nat.land Nat.land' /--`ldiff' a b` performs bitwise set difference. For each corresponding pair of bits taken as booleans, say `aᵢ` and `bᵢ`, it applies the