Nat.bit1_ne_zero
theorem Nat.bit1_ne_zero : ∀ (n : ℕ), bit1 n ≠ 0
The theorem `Nat.bit1_ne_zero` states that for every natural number `n`, the binary representation `bit1 n` is not equal to zero. In other words, the binary representation with an odd number of 1's `bit1 n` (which equates to `2n + 1` in natural numbers) will never be zero for any natural number `n`.
More concisely: For all natural numbers n, the first binary digit of n, represented as `bit1 n` in Lean, is non-zero. Equivalently, the binary representation of a natural number has an odd number of 1's.
|
Nat.bit0_succ_eq
theorem Nat.bit0_succ_eq : ∀ (n : ℕ), bit0 n.succ = (bit0 n).succ.succ
The theorem `Nat.bit0_succ_eq` states that for all natural numbers `n`, the value of applying the `bit0` operation (which doubles the input) to the successor (`Nat.succ`) of `n` is equal to the successor of the successor of `bit0 n`. In other words, doubling the number `n+1` is the same as adding two to the double of `n`.
More concisely: For all natural numbers `n`, `bit0 (Nat.succ n) = Nat.succ (bit0 n)`.
|
Nat.bit0_ne_zero
theorem Nat.bit0_ne_zero : ∀ {n : ℕ}, n ≠ 0 → bit0 n ≠ 0
This theorem states that for all natural numbers `n`, if `n` is not equal to zero, then the double of `n` (represented by `bit0 n`) is also not equal to zero. Here, `bit0` is a function that takes a number and returns its double. In mathematical terms, the theorem asserts that for any natural number $n$, if $n \neq 0$, then $2n \neq 0$.
More concisely: For all natural numbers $n$, if $n \neq 0$, then $2n \neq 0$.
|