Skip to content

Commit

Permalink
fix: Fix aligns (#2781)
Browse files Browse the repository at this point in the history
  • Loading branch information
Komyyy committed Mar 11, 2023
1 parent 7edeec3 commit 416bfc2
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 3 deletions.
2 changes: 2 additions & 0 deletions Mathlib/Algebra/GroupWithZero/Defs.lean
Expand Up @@ -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₀`. -/
Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Init/Data/Nat/Bitwise.lean
Expand Up @@ -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
Expand Down

0 comments on commit 416bfc2

Please sign in to comment.