Properties of the binary representation of integers #
theorem
PosNum.cmp_to_nat
(m : PosNum)
(n : PosNum)
:
Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
theorem
Num.ofNat'_bit
(b : Bool)
(n : ℕ)
:
Num.ofNat' (Nat.bit b n) = (bif b then Num.bit1 else Num.bit0) (Num.ofNat' n)
@[simp]
This tactic tries to turn an (in)equality about Num
s to one about Nat
s by rewriting.
example (n : Num) (m : Num) : n ≤ n + m := by
transfer_rw
exact Nat.le_add_right _ _
Equations
- Num.transfer_rw = Lean.ParserDescr.node `Num.transfer_rw 1024 (Lean.ParserDescr.nonReservedSymbol "transfer_rw" false)
Instances For
This tactic tries to prove (in)equalities about Num
s by transferring them to the Nat
world and
then trying to call simp
.
example (n : Num) (m : Num) : n ≤ n + m := by transfer
Equations
- Num.transfer = Lean.ParserDescr.node `Num.transfer 1024 (Lean.ParserDescr.nonReservedSymbol "transfer" false)
Instances For
Equations
Equations
Equations
- One or more equations did not get rendered due to their size.
@[deprecated Num.of_natCast]
Alias of Num.of_natCast
.
This tactic tries to turn an (in)equality about PosNum
s to one about Nat
s by rewriting.
example (n : PosNum) (m : PosNum) : n ≤ n + m := by
transfer_rw
exact Nat.le_add_right _ _
Equations
- PosNum.transfer_rw = Lean.ParserDescr.node `PosNum.transfer_rw 1024 (Lean.ParserDescr.nonReservedSymbol "transfer_rw" false)
Instances For
This tactic tries to prove (in)equalities about PosNum
s by transferring them to the Nat
world
and then trying to call simp
.
example (n : PosNum) (m : PosNum) : n ≤ n + m := by transfer
Equations
- PosNum.transfer = Lean.ParserDescr.node `PosNum.transfer 1024 (Lean.ParserDescr.nonReservedSymbol "transfer" false)
Instances For
Equations
- PosNum.linearOrder = LinearOrder.mk PosNum.linearOrder.proof_5 inferInstance inferInstance inferInstance PosNum.linearOrder.proof_6 PosNum.linearOrder.proof_7 PosNum.linearOrder.proof_8
@[simp]
@[simp]
@[simp]
theorem
PosNum.cast_inj
{α : Type u_1}
[AddMonoidWithOne α]
[CharZero α]
{m : PosNum}
{n : PosNum}
:
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Num.castNum_eq_bitwise
{f : Num → Num → Num}
{g : Bool → Bool → Bool}
(p : PosNum → PosNum → Num)
(gff : g false false = false)
(f00 : f 0 0 = 0)
(f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0)
(fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0)
(fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n)
(p11 : p 1 1 = bif g true true then 1 else 0)
(p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = Num.bit (g true b) (bif g false true then Num.pos n else 0))
(pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = Num.bit (g a true) (bif g true false then Num.pos m else 0))
(pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = Num.bit (g a b) (p m n))
(m : Num)
(n : Num)
:
↑(f m n) = Nat.bitwise g ↑m ↑n
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Num.cast_ofZNum
{α : Type u_1}
[AddGroupWithOne α]
(n : ZNum)
:
↑(Num.ofZNum n) = ↑(↑n).toNat
@[simp]
@[simp]
theorem
ZNum.cmp_to_int
(m : ZNum)
(n : ZNum)
:
Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
@[simp]
@[simp]
@[simp]
This tactic tries to turn an (in)equality about ZNum
s to one about Int
s by rewriting.
example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
transfer_rw
exact le_add_of_nonneg_right (mul_self_nonneg _)
Equations
- ZNum.transfer_rw = Lean.ParserDescr.node `ZNum.transfer_rw 1024 (Lean.ParserDescr.nonReservedSymbol "transfer_rw" false)
Instances For
This tactic tries to prove (in)equalities about ZNum
s by transferring them to the Int
world and
then trying to call simp
.
example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
transfer
exact mul_self_nonneg _
Equations
- ZNum.transfer = Lean.ParserDescr.node `ZNum.transfer 1024 (Lean.ParserDescr.nonReservedSymbol "transfer" false)
Instances For
@[deprecated ZNum.of_intCast]
Alias of ZNum.of_intCast
.
@[deprecated ZNum.of_natCast]
Alias of ZNum.of_natCast
.
theorem
Num.gcd_to_nat_aux
{n : ℕ}
{a : Num}
{b : Num}
:
a ≤ b → (a * b).natSize ≤ n → ↑(Num.gcdAux n a b) = (↑a).gcd ↑b
Equations
- x✝.decidableDvd x = decidable_of_iff' (x % x✝ = 0) ⋯
Equations
- x✝.decidableDvd x = decidable_of_iff' (x % x✝ = 0) ⋯
Equations
- SNum.lt = { lt := fun (a b : SNum) => Int.ofSnum a < Int.ofSnum b }
Equations
- SNum.le = { le := fun (a b : SNum) => Int.ofSnum a ≤ Int.ofSnum b }