Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.pow2_defined
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
:
πΊβ-Predicate LO.Arith.Pow2 via LO.FirstOrder.Arith.pow2Def
instance
LO.Arith.pow2_definable
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
:
πΊβ-Predicate LO.Arith.Pow2
Equations
- β― = β―
theorem
LO.Arith.Pow2.pos
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
(h : LO.Arith.Pow2 a)
:
0 < a
theorem
LO.Arith.Pow2.dvd
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
(h : LO.Arith.Pow2 a)
{r : V}
(hr : r β€ a)
:
@[simp]
@[simp]
theorem
LO.Arith.Pow2.two_dvd
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
(h : LO.Arith.Pow2 a)
(lt : 1 < a)
:
2 β£ a
theorem
LO.Arith.Pow2.two_dvd'
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
(h : LO.Arith.Pow2 a)
(lt : a β 1)
:
2 β£ a
theorem
LO.Arith.Pow2.of_dvd
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
{b : V}
(h : b β£ a)
:
LO.Arith.Pow2 a β LO.Arith.Pow2 b
theorem
LO.Arith.pow2_mul_two
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
:
LO.Arith.Pow2 (2 * a) β LO.Arith.Pow2 a
theorem
LO.Arith.pow2_mul_four
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
:
LO.Arith.Pow2 (4 * a) β LO.Arith.Pow2 a
theorem
LO.Arith.Pow2.elim
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{p : V}
:
LO.Arith.Pow2 p β p = 1 β¨ β (q : V), p = 2 * q β§ LO.Arith.Pow2 q
@[simp]
theorem
LO.Arith.Pow2.div_two
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{p : V}
(h : LO.Arith.Pow2 p)
(ne : p β 1)
:
LO.Arith.Pow2 (p / 2)
theorem
LO.Arith.Pow2.two_mul_div_two
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{p : V}
(h : LO.Arith.Pow2 p)
(ne : p β 1)
:
theorem
LO.Arith.Pow2.div_two_mul_two
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{p : V}
(h : LO.Arith.Pow2 p)
(ne : p β 1)
:
theorem
LO.Arith.Pow2.elim'
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{p : V}
:
LO.Arith.Pow2 p β p = 1 β¨ 1 < p β§ β (q : V), p = 2 * q β§ LO.Arith.Pow2 q
$\mathrm{LenBit} (2^i, a) \iff \text{$i$th-bit of $a$ is $1$}$.
Equations
- LO.Arith.LenBit i a = Β¬2 β£ a / i
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.lenbit_defined
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
:
πΊβ-Relation LO.Arith.LenBit via LO.FirstOrder.Arith.lenbitDef
@[simp]
theorem
LO.Arith.lenbit_defined_iff
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
(v : Fin 2 β V)
:
Equations
- β― = β―
theorem
LO.Arith.LenBit.le
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{i : V}
{a : V}
(h : LO.Arith.LenBit i a)
:
i β€ a
theorem
LO.Arith.not_lenbit_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{i : V}
{a : V}
(h : a < i)
:
@[simp]
@[simp]
theorem
LO.Arith.LenBit.one
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
(a : V)
:
LO.Arith.LenBit 1 a β Β¬2 β£ a
theorem
LO.Arith.LenBit.iff_rem
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{i : V}
{a : V}
:
LO.Arith.LenBit i a β a / i % 2 = 1
theorem
LO.Arith.not_lenbit_iff_rem
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{i : V}
{a : V}
:
@[simp]
theorem
LO.Arith.LenBit.self
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
(pos : 0 < a)
:
LO.Arith.LenBit a a
theorem
LO.Arith.LenBit.mod
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{i : V}
{a : V}
{k : V}
(h : 2 * i β£ k)
:
LO.Arith.LenBit i (a % k) β LO.Arith.LenBit i a
@[simp]
theorem
LO.Arith.LenBit.mod_two_mul_self
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
{i : V}
:
LO.Arith.LenBit i (a % (2 * i)) β LO.Arith.LenBit i a
theorem
LO.Arith.LenBit.add
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{i : V}
{a : V}
{b : V}
(h : 2 * i β£ b)
:
LO.Arith.LenBit i (a + b) β LO.Arith.LenBit i a
theorem
LO.Arith.LenBit.add_self
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{i : V}
{a : V}
(h : a < i)
:
LO.Arith.LenBit i (a + i)
theorem
LO.Arith.LenBit.add_self_of_not_lenbit
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
{i : V}
(pos : 0 < i)
(h : Β¬LO.Arith.LenBit i a)
:
LO.Arith.LenBit i (a + i)
theorem
LO.Arith.LenBit.add_self_of_lenbit
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
{i : V}
(pos : 0 < i)
(h : LO.Arith.LenBit i a)
:
Β¬LO.Arith.LenBit i (a + i)
theorem
LO.Arith.LenBit.sub_self_of_lenbit
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* πopen]
{a : V}
{i : V}
(pos : 0 < i)
(h : LO.Arith.LenBit i a)
:
Β¬LO.Arith.LenBit i (a - i)
theorem
LO.Arith.Pow2.mul
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{b : V}
(ha : LO.Arith.Pow2 a)
(hb : LO.Arith.Pow2 b)
:
LO.Arith.Pow2 (a * b)
@[simp]
theorem
LO.Arith.Pow2.mul_iff
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{b : V}
:
LO.Arith.Pow2 (a * b) β LO.Arith.Pow2 a β§ LO.Arith.Pow2 b
@[simp]
theorem
LO.Arith.Pow2.sq_iff
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
:
LO.Arith.Pow2 (a ^ 2) β LO.Arith.Pow2 a
theorem
LO.Arith.Pow2.sq
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
:
LO.Arith.Pow2 a β LO.Arith.Pow2 (a ^ 2)
theorem
LO.Arith.Pow2.dvd_of_le
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{b : V}
(ha : LO.Arith.Pow2 a)
(hb : LO.Arith.Pow2 b)
:
theorem
LO.Arith.Pow2.le_iff_dvd
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{b : V}
(ha : LO.Arith.Pow2 a)
(hb : LO.Arith.Pow2 b)
:
theorem
LO.Arith.Pow2.two_le
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
(pa : LO.Arith.Pow2 a)
(ne1 : a β 1)
:
2 β€ a
theorem
LO.Arith.Pow2.le_iff_lt_two
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{b : V}
(ha : LO.Arith.Pow2 a)
(hb : LO.Arith.Pow2 b)
:
theorem
LO.Arith.Pow2.lt_iff_two_mul_le
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{b : V}
(ha : LO.Arith.Pow2 a)
(hb : LO.Arith.Pow2 b)
:
theorem
LO.Arith.Pow2.sq_or_dsq
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
(pa : LO.Arith.Pow2 a)
:
theorem
LO.Arith.Pow2.sqrt
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
(h : LO.Arith.Pow2 a)
(hsq : (βa) ^ 2 = a)
:
LO.Arith.Pow2 (βa)
@[simp]
theorem
LO.Arith.Pow2.four_le
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{i : V}
(hi : LO.Arith.Pow2 i)
(lt : 2 < i)
:
4 β€ i
theorem
LO.Arith.Pow2.mul_add_lt_of_mul_lt_of_pos
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{b : V}
{p : V}
{q : V}
(hp : LO.Arith.Pow2 p)
(hq : LO.Arith.Pow2 q)
(h : a * p < q)
(hb : b < p)
(hbq : b < q)
:
theorem
LO.Arith.LenBit.mod_pow2
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{i : V}
{j : V}
(pi : LO.Arith.Pow2 i)
(pj : LO.Arith.Pow2 j)
(h : i < j)
:
LO.Arith.LenBit i (a % j) β LO.Arith.LenBit i a
theorem
LO.Arith.LenBit.add_pow2
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{i : V}
{j : V}
(pi : LO.Arith.Pow2 i)
(pj : LO.Arith.Pow2 j)
(h : i < j)
:
LO.Arith.LenBit i (a + j) β LO.Arith.LenBit i a
theorem
LO.Arith.LenBit.add_pow2_iff_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{i : V}
{j : V}
(pi : LO.Arith.Pow2 i)
(pj : LO.Arith.Pow2 j)
(h : a < j)
:
LO.Arith.LenBit i (a + j) β i = j β¨ LO.Arith.LenBit i a
theorem
LO.Arith.lenbit_iff_add_mul
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{i : V}
{a : V}
(hi : LO.Arith.Pow2 i)
:
theorem
LO.Arith.not_lenbit_iff_add_mul
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{i : V}
{a : V}
(hi : LO.Arith.Pow2 i)
:
theorem
LO.Arith.lenbit_mul_add
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{i : V}
{j : V}
{a : V}
{r : V}
(pi : LO.Arith.Pow2 i)
(pj : LO.Arith.Pow2 j)
(hr : r < j)
:
LO.Arith.LenBit (i * j) (a * j + r) β LO.Arith.LenBit i a
theorem
LO.Arith.lenbit_add_pow2_iff_of_not_lenbit
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{i : V}
{j : V}
(pi : LO.Arith.Pow2 i)
(pj : LO.Arith.Pow2 j)
(h : Β¬LO.Arith.LenBit j a)
:
LO.Arith.LenBit i (a + j) β i = j β¨ LO.Arith.LenBit i a
theorem
LO.Arith.lenbit_sub_pow2_iff_of_lenbit
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{a : V}
{i : V}
{j : V}
(pi : LO.Arith.Pow2 i)
(pj : LO.Arith.Pow2 j)
(h : LO.Arith.LenBit j a)
:
LO.Arith.LenBit i (a - j) β i β j β§ LO.Arith.LenBit i a