michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/data/rat/basic): define pow before migrate

Browse source
This commit is contained in:
Jeremy Avigad 2015-07-31 22:42:11 +03:00 committed by Leonardo de Moura
parent 343b9e62c7
commit 36c7aad6ee
2 changed files with 7 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/data/rat/basic.lean
View file

@ -512,12 +512,17 @@ section migrate_algebra
has_decidable_eq := has_decidable_eq⦄ has_decidable_eq := has_decidable_eq⦄
local attribute rat.discrete_field [instance] local attribute rat.discrete_field [instance]
definition divide (a b : rat) := algebra.divide a b definition divide (a b : rat) := algebra.divide a b
infix `/` := divide infix [priority rat.prio] `/` := divide
definition dvd (a b : rat) := algebra.dvd a b definition dvd (a b : rat) := algebra.dvd a b
definition pow (a : ℚ) (n : ℕ) : ℚ := algebra.pow a n
infix [priority rat.prio] ^ := pow
migrate from algebra with rat migrate from algebra with rat
replacing sub → rat.sub, divide → divide, dvd → dvd replacing sub → rat.sub, divide → divide, dvd → dvd, pow → pow
end migrate_algebra end migrate_algebra
@ -537,5 +542,4 @@ decidable.by_cases
by rewrite [Hc, !int.mul_div_cancel_left bnz, mul.comm]), by rewrite [Hc, !int.mul_div_cancel_left bnz, mul.comm]),
iff.mpr (eq_div_iff_mul_eq bnz') H') iff.mpr (eq_div_iff_mul_eq bnz') H')
end rat end rat

5
library/data/real/complete.lean
View file

@ -20,13 +20,11 @@ open -[coercions] nat
open eq.ops open eq.ops
open pnat open pnat
local notation 2 := subtype.tag (nat.of_num 2) dec_trivial local notation 2 := subtype.tag (nat.of_num 2) dec_trivial
local notation 3 := subtype.tag (nat.of_num 3) dec_trivial local notation 3 := subtype.tag (nat.of_num 3) dec_trivial
namespace s namespace s
theorem rat_approx_l1 {s : seq} (H : regular s) : theorem rat_approx_l1 {s : seq} (H : regular s) :
∀ n : ℕ+, ∃ q : ℚ, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → abs (s m - q) ≤ n⁻¹ := ∀ n : ℕ+, ∃ q : ℚ, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → abs (s m - q) ≤ n⁻¹ :=
begin begin
@ -749,9 +747,6 @@ theorem over_succ (n : ℕ) : over_seq (succ n) =
apply H apply H
end end
-- ???
theorem rat.pow_add (a : ℚ) (m : ℕ) : ∀ n, rat.pow a (m + n) = rat.pow a m * rat.pow a n := rat.pow_add a m
theorem width (n : ℕ) : over_seq n - under_seq n = (over - under) / (rat.pow 2 n) := theorem width (n : ℕ) : over_seq n - under_seq n = (over - under) / (rat.pow 2 n) :=
nat.induction_on n nat.induction_on n
(by xrewrite [over_0, under_0, rat.pow_zero, rat.div_one]) (by xrewrite [over_0, under_0, rat.pow_zero, rat.div_one])