From 1f7d0614e537bdfa2b527b3d3750aa5f96028214 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 3 May 2023 20:59:26 +0200 Subject: [PATCH 1/8] feat: port Algebra.ContinuedFractions.Translations From 34d9f82a0d29b0e48467fca80ebc2276f799c7a5 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 3 May 2023 20:59:26 +0200 Subject: [PATCH 2/8] Initial file copy from mathport --- .../ContinuedFractions/Translations.lean | 191 ++++++++++++++++++ 1 file changed, 191 insertions(+) create mode 100644 Mathlib/Algebra/ContinuedFractions/Translations.lean diff --git a/Mathlib/Algebra/ContinuedFractions/Translations.lean b/Mathlib/Algebra/ContinuedFractions/Translations.lean new file mode 100644 index 0000000000000..9b03f3001853b --- /dev/null +++ b/Mathlib/Algebra/ContinuedFractions/Translations.lean @@ -0,0 +1,191 @@ +/- +Copyright (c) 2019 Kevin Kappelmann. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kevin Kappelmann + +! This file was ported from Lean 3 source module algebra.continued_fractions.translations +! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.Algebra.ContinuedFractions.Basic + +/-! +# Basic Translation Lemmas Between Functions Defined for Continued Fractions + +## Summary + +Some simple translation lemmas between the different definitions of functions defined in +`algebra.continued_fractions.basic`. +-/ + + +namespace GeneralizedContinuedFraction + +/- ./././Mathport/Syntax/Translate/Command.lean:229:11: unsupported: unusual advanced open style -/ +section General + +/-! +### Translations Between General Access Functions + +Here we give some basic translations that hold by definition between the various methods that allow +us to access the numerators and denominators of a continued fraction. +-/ + + +variable {α : Type _} {g : GeneralizedContinuedFraction α} {n : ℕ} + +theorem terminatedAt_iff_s_terminatedAt : g.TerminatedAt n ↔ g.s.TerminatedAt n := by rfl +#align generalized_continued_fraction.terminated_at_iff_s_terminated_at GeneralizedContinuedFraction.terminatedAt_iff_s_terminatedAt + +theorem terminatedAt_iff_s_none : g.TerminatedAt n ↔ g.s.get? n = none := by rfl +#align generalized_continued_fraction.terminated_at_iff_s_none GeneralizedContinuedFraction.terminatedAt_iff_s_none + +theorem part_num_none_iff_s_none : g.partialNumerators.get? n = none ↔ g.s.get? n = none := by + cases s_nth_eq : g.s.nth n <;> simp [partial_numerators, s_nth_eq] +#align generalized_continued_fraction.part_num_none_iff_s_none GeneralizedContinuedFraction.part_num_none_iff_s_none + +theorem terminatedAt_iff_part_num_none : g.TerminatedAt n ↔ g.partialNumerators.get? n = none := by + rw [terminated_at_iff_s_none, part_num_none_iff_s_none] +#align generalized_continued_fraction.terminated_at_iff_part_num_none GeneralizedContinuedFraction.terminatedAt_iff_part_num_none + +theorem part_denom_none_iff_s_none : g.partialDenominators.get? n = none ↔ g.s.get? n = none := by + cases s_nth_eq : g.s.nth n <;> simp [partial_denominators, s_nth_eq] +#align generalized_continued_fraction.part_denom_none_iff_s_none GeneralizedContinuedFraction.part_denom_none_iff_s_none + +theorem terminatedAt_iff_part_denom_none : g.TerminatedAt n ↔ g.partialDenominators.get? n = none := + by rw [terminated_at_iff_s_none, part_denom_none_iff_s_none] +#align generalized_continued_fraction.terminated_at_iff_part_denom_none GeneralizedContinuedFraction.terminatedAt_iff_part_denom_none + +theorem part_num_eq_s_a {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) : + g.partialNumerators.get? n = some gp.a := by simp [partial_numerators, s_nth_eq] +#align generalized_continued_fraction.part_num_eq_s_a GeneralizedContinuedFraction.part_num_eq_s_a + +theorem part_denom_eq_s_b {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) : + g.partialDenominators.get? n = some gp.b := by simp [partial_denominators, s_nth_eq] +#align generalized_continued_fraction.part_denom_eq_s_b GeneralizedContinuedFraction.part_denom_eq_s_b + +theorem exists_s_a_of_part_num {a : α} (nth_part_num_eq : g.partialNumerators.get? n = some a) : + ∃ gp, g.s.get? n = some gp ∧ gp.a = a := by + simpa [partial_numerators, seq.map_nth] using nth_part_num_eq +#align generalized_continued_fraction.exists_s_a_of_part_num GeneralizedContinuedFraction.exists_s_a_of_part_num + +theorem exists_s_b_of_part_denom {b : α} + (nth_part_denom_eq : g.partialDenominators.get? n = some b) : + ∃ gp, g.s.get? n = some gp ∧ gp.b = b := by + simpa [partial_denominators, seq.map_nth] using nth_part_denom_eq +#align generalized_continued_fraction.exists_s_b_of_part_denom GeneralizedContinuedFraction.exists_s_b_of_part_denom + +end General + +section WithDivisionRing + +/-! +### Translations Between Computational Functions + +Here we give some basic translations that hold by definition for the computational methods of a +continued fraction. +-/ + + +variable {K : Type _} {g : GeneralizedContinuedFraction K} {n : ℕ} [DivisionRing K] + +theorem nth_cont_eq_succ_nth_cont_aux : g.continuants n = g.continuantsAux (n + 1) := + rfl +#align generalized_continued_fraction.nth_cont_eq_succ_nth_cont_aux GeneralizedContinuedFraction.nth_cont_eq_succ_nth_cont_aux + +theorem num_eq_conts_a : g.numerators n = (g.continuants n).a := + rfl +#align generalized_continued_fraction.num_eq_conts_a GeneralizedContinuedFraction.num_eq_conts_a + +theorem denom_eq_conts_b : g.denominators n = (g.continuants n).b := + rfl +#align generalized_continued_fraction.denom_eq_conts_b GeneralizedContinuedFraction.denom_eq_conts_b + +theorem convergent_eq_num_div_denom : g.convergents n = g.numerators n / g.denominators n := + rfl +#align generalized_continued_fraction.convergent_eq_num_div_denom GeneralizedContinuedFraction.convergent_eq_num_div_denom + +theorem convergent_eq_conts_a_div_conts_b : + g.convergents n = (g.continuants n).a / (g.continuants n).b := + rfl +#align generalized_continued_fraction.convergent_eq_conts_a_div_conts_b GeneralizedContinuedFraction.convergent_eq_conts_a_div_conts_b + +theorem exists_conts_a_of_num {A : K} (nth_num_eq : g.numerators n = A) : + ∃ conts, g.continuants n = conts ∧ conts.a = A := by simpa +#align generalized_continued_fraction.exists_conts_a_of_num GeneralizedContinuedFraction.exists_conts_a_of_num + +theorem exists_conts_b_of_denom {B : K} (nth_denom_eq : g.denominators n = B) : + ∃ conts, g.continuants n = conts ∧ conts.b = B := by simpa +#align generalized_continued_fraction.exists_conts_b_of_denom GeneralizedContinuedFraction.exists_conts_b_of_denom + +@[simp] +theorem zeroth_continuant_aux_eq_one_zero : g.continuantsAux 0 = ⟨1, 0⟩ := + rfl +#align generalized_continued_fraction.zeroth_continuant_aux_eq_one_zero GeneralizedContinuedFraction.zeroth_continuant_aux_eq_one_zero + +@[simp] +theorem first_continuant_aux_eq_h_one : g.continuantsAux 1 = ⟨g.h, 1⟩ := + rfl +#align generalized_continued_fraction.first_continuant_aux_eq_h_one GeneralizedContinuedFraction.first_continuant_aux_eq_h_one + +@[simp] +theorem zeroth_continuant_eq_h_one : g.continuants 0 = ⟨g.h, 1⟩ := + rfl +#align generalized_continued_fraction.zeroth_continuant_eq_h_one GeneralizedContinuedFraction.zeroth_continuant_eq_h_one + +@[simp] +theorem zeroth_numerator_eq_h : g.numerators 0 = g.h := + rfl +#align generalized_continued_fraction.zeroth_numerator_eq_h GeneralizedContinuedFraction.zeroth_numerator_eq_h + +@[simp] +theorem zeroth_denominator_eq_one : g.denominators 0 = 1 := + rfl +#align generalized_continued_fraction.zeroth_denominator_eq_one GeneralizedContinuedFraction.zeroth_denominator_eq_one + +@[simp] +theorem zeroth_convergent_eq_h : g.convergents 0 = g.h := by + simp [convergent_eq_num_div_denom, num_eq_conts_a, denom_eq_conts_b, div_one] +#align generalized_continued_fraction.zeroth_convergent_eq_h GeneralizedContinuedFraction.zeroth_convergent_eq_h + +theorem second_continuant_aux_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : + g.continuantsAux 2 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by + simp [zeroth_s_eq, continuants_aux, next_continuants, next_denominator, next_numerator] +#align generalized_continued_fraction.second_continuant_aux_eq GeneralizedContinuedFraction.second_continuant_aux_eq + +theorem first_continuant_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : + g.continuants 1 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by + simp [nth_cont_eq_succ_nth_cont_aux, second_continuant_aux_eq zeroth_s_eq] +#align generalized_continued_fraction.first_continuant_eq GeneralizedContinuedFraction.first_continuant_eq + +theorem first_numerator_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : + g.numerators 1 = gp.b * g.h + gp.a := by simp [num_eq_conts_a, first_continuant_eq zeroth_s_eq] +#align generalized_continued_fraction.first_numerator_eq GeneralizedContinuedFraction.first_numerator_eq + +theorem first_denominator_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : + g.denominators 1 = gp.b := by simp [denom_eq_conts_b, first_continuant_eq zeroth_s_eq] +#align generalized_continued_fraction.first_denominator_eq GeneralizedContinuedFraction.first_denominator_eq + +@[simp] +theorem zeroth_convergent'_aux_eq_zero {s : Seq <| Pair K} : convergents'Aux s 0 = 0 := + rfl +#align generalized_continued_fraction.zeroth_convergent'_aux_eq_zero GeneralizedContinuedFraction.zeroth_convergent'_aux_eq_zero + +@[simp] +theorem zeroth_convergent'_eq_h : g.convergents' 0 = g.h := by simp [convergents'] +#align generalized_continued_fraction.zeroth_convergent'_eq_h GeneralizedContinuedFraction.zeroth_convergent'_eq_h + +theorem convergents'Aux_succ_none {s : Seq (Pair K)} (h : s.headI = none) (n : ℕ) : + convergents'Aux s (n + 1) = 0 := by rw [convergents'_aux, h, convergents'_aux._match_1] +#align generalized_continued_fraction.convergents'_aux_succ_none GeneralizedContinuedFraction.convergents'Aux_succ_none + +theorem convergents'Aux_succ_some {s : Seq (Pair K)} {p : Pair K} (h : s.headI = some p) (n : ℕ) : + convergents'Aux s (n + 1) = p.a / (p.b + convergents'Aux s.tail n) := by + rw [convergents'_aux, h, convergents'_aux._match_1] +#align generalized_continued_fraction.convergents'_aux_succ_some GeneralizedContinuedFraction.convergents'Aux_succ_some + +end WithDivisionRing + +end GeneralizedContinuedFraction + From 2972490e37cbeb8e0a7516aacd8572efb676505f Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 3 May 2023 20:59:26 +0200 Subject: [PATCH 3/8] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/Algebra/ContinuedFractions/Translations.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib.lean b/Mathlib.lean index f6b6f903c32aa..33b56ac9ce43b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -52,6 +52,7 @@ import Mathlib.Algebra.CharZero.Infinite import Mathlib.Algebra.CharZero.Lemmas import Mathlib.Algebra.CharZero.Quotient import Mathlib.Algebra.ContinuedFractions.Basic +import Mathlib.Algebra.ContinuedFractions.Translations import Mathlib.Algebra.CovariantAndContravariant import Mathlib.Algebra.CubicDiscriminant import Mathlib.Algebra.DirectSum.Basic diff --git a/Mathlib/Algebra/ContinuedFractions/Translations.lean b/Mathlib/Algebra/ContinuedFractions/Translations.lean index 9b03f3001853b..22e41d6a277f5 100644 --- a/Mathlib/Algebra/ContinuedFractions/Translations.lean +++ b/Mathlib/Algebra/ContinuedFractions/Translations.lean @@ -8,7 +8,7 @@ Authors: Kevin Kappelmann ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Algebra.ContinuedFractions.Basic +import Mathlib.Algebra.ContinuedFractions.Basic /-! # Basic Translation Lemmas Between Functions Defined for Continued Fractions From 65c4d86deb1495ba292750d8c0f99eccafe25859 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 3 May 2023 21:06:13 +0200 Subject: [PATCH 4/8] starting --- .../ContinuedFractions/Translations.lean | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/Mathlib/Algebra/ContinuedFractions/Translations.lean b/Mathlib/Algebra/ContinuedFractions/Translations.lean index 22e41d6a277f5..2e87539978443 100644 --- a/Mathlib/Algebra/ContinuedFractions/Translations.lean +++ b/Mathlib/Algebra/ContinuedFractions/Translations.lean @@ -23,7 +23,8 @@ Some simple translation lemmas between the different definitions of functions de namespace GeneralizedContinuedFraction /- ./././Mathport/Syntax/Translate/Command.lean:229:11: unsupported: unusual advanced open style -/ -section General +-- porting note: TODO +-- section General /-! ### Translations Between General Access Functions @@ -42,41 +43,41 @@ theorem terminatedAt_iff_s_none : g.TerminatedAt n ↔ g.s.get? n = none := by r #align generalized_continued_fraction.terminated_at_iff_s_none GeneralizedContinuedFraction.terminatedAt_iff_s_none theorem part_num_none_iff_s_none : g.partialNumerators.get? n = none ↔ g.s.get? n = none := by - cases s_nth_eq : g.s.nth n <;> simp [partial_numerators, s_nth_eq] + cases s_nth_eq : g.s.get? n <;> simp [partialNumerators, s_nth_eq] #align generalized_continued_fraction.part_num_none_iff_s_none GeneralizedContinuedFraction.part_num_none_iff_s_none theorem terminatedAt_iff_part_num_none : g.TerminatedAt n ↔ g.partialNumerators.get? n = none := by - rw [terminated_at_iff_s_none, part_num_none_iff_s_none] + rw [terminatedAt_iff_s_none, part_num_none_iff_s_none] #align generalized_continued_fraction.terminated_at_iff_part_num_none GeneralizedContinuedFraction.terminatedAt_iff_part_num_none theorem part_denom_none_iff_s_none : g.partialDenominators.get? n = none ↔ g.s.get? n = none := by - cases s_nth_eq : g.s.nth n <;> simp [partial_denominators, s_nth_eq] + cases s_nth_eq : g.s.get? n <;> simp [partialDenominators, s_nth_eq] #align generalized_continued_fraction.part_denom_none_iff_s_none GeneralizedContinuedFraction.part_denom_none_iff_s_none theorem terminatedAt_iff_part_denom_none : g.TerminatedAt n ↔ g.partialDenominators.get? n = none := - by rw [terminated_at_iff_s_none, part_denom_none_iff_s_none] + by rw [terminatedAt_iff_s_none, part_denom_none_iff_s_none] #align generalized_continued_fraction.terminated_at_iff_part_denom_none GeneralizedContinuedFraction.terminatedAt_iff_part_denom_none theorem part_num_eq_s_a {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) : - g.partialNumerators.get? n = some gp.a := by simp [partial_numerators, s_nth_eq] + g.partialNumerators.get? n = some gp.a := by simp [partialNumerators, s_nth_eq] #align generalized_continued_fraction.part_num_eq_s_a GeneralizedContinuedFraction.part_num_eq_s_a theorem part_denom_eq_s_b {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) : - g.partialDenominators.get? n = some gp.b := by simp [partial_denominators, s_nth_eq] + g.partialDenominators.get? n = some gp.b := by simp [partialDenominators, s_nth_eq] #align generalized_continued_fraction.part_denom_eq_s_b GeneralizedContinuedFraction.part_denom_eq_s_b theorem exists_s_a_of_part_num {a : α} (nth_part_num_eq : g.partialNumerators.get? n = some a) : ∃ gp, g.s.get? n = some gp ∧ gp.a = a := by - simpa [partial_numerators, seq.map_nth] using nth_part_num_eq + simpa [partialNumerators, Stream'.Seq.map_get?] using nth_part_num_eq #align generalized_continued_fraction.exists_s_a_of_part_num GeneralizedContinuedFraction.exists_s_a_of_part_num theorem exists_s_b_of_part_denom {b : α} (nth_part_denom_eq : g.partialDenominators.get? n = some b) : ∃ gp, g.s.get? n = some gp ∧ gp.b = b := by - simpa [partial_denominators, seq.map_nth] using nth_part_denom_eq + simpa [partialDenominators, Stream'.Seq.map_get?] using nth_part_denom_eq #align generalized_continued_fraction.exists_s_b_of_part_denom GeneralizedContinuedFraction.exists_s_b_of_part_denom -end General +-- end General section WithDivisionRing @@ -188,4 +189,3 @@ theorem convergents'Aux_succ_some {s : Seq (Pair K)} {p : Pair K} (h : s.headI = end WithDivisionRing end GeneralizedContinuedFraction - From 415544bace9ccbe0e0d464f96baa8656a1dd4442 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 3 May 2023 21:18:02 +0200 Subject: [PATCH 5/8] builds --- .../ContinuedFractions/Translations.lean | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/ContinuedFractions/Translations.lean b/Mathlib/Algebra/ContinuedFractions/Translations.lean index 2e87539978443..b9fd475568abe 100644 --- a/Mathlib/Algebra/ContinuedFractions/Translations.lean +++ b/Mathlib/Algebra/ContinuedFractions/Translations.lean @@ -152,12 +152,14 @@ theorem zeroth_convergent_eq_h : g.convergents 0 = g.h := by theorem second_continuant_aux_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : g.continuantsAux 2 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by - simp [zeroth_s_eq, continuants_aux, next_continuants, next_denominator, next_numerator] + simp [zeroth_s_eq, continuantsAux, nextContinuants, nextDenominator, nextNumerator] #align generalized_continued_fraction.second_continuant_aux_eq GeneralizedContinuedFraction.second_continuant_aux_eq theorem first_continuant_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : g.continuants 1 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by - simp [nth_cont_eq_succ_nth_cont_aux, second_continuant_aux_eq zeroth_s_eq] + simp [nth_cont_eq_succ_nth_cont_aux] + -- porting note: simp used to work here, but now it can't figure out that 1 + 1 = 2 + convert second_continuant_aux_eq zeroth_s_eq #align generalized_continued_fraction.first_continuant_eq GeneralizedContinuedFraction.first_continuant_eq theorem first_numerator_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : @@ -169,7 +171,8 @@ theorem first_denominator_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) #align generalized_continued_fraction.first_denominator_eq GeneralizedContinuedFraction.first_denominator_eq @[simp] -theorem zeroth_convergent'_aux_eq_zero {s : Seq <| Pair K} : convergents'Aux s 0 = 0 := +theorem zeroth_convergent'_aux_eq_zero {s : Stream'.Seq <| Pair K} : + convergents'Aux s 0 = (0 : K) := rfl #align generalized_continued_fraction.zeroth_convergent'_aux_eq_zero GeneralizedContinuedFraction.zeroth_convergent'_aux_eq_zero @@ -177,15 +180,16 @@ theorem zeroth_convergent'_aux_eq_zero {s : Seq <| Pair K} : convergents'Aux s 0 theorem zeroth_convergent'_eq_h : g.convergents' 0 = g.h := by simp [convergents'] #align generalized_continued_fraction.zeroth_convergent'_eq_h GeneralizedContinuedFraction.zeroth_convergent'_eq_h -theorem convergents'Aux_succ_none {s : Seq (Pair K)} (h : s.headI = none) (n : ℕ) : - convergents'Aux s (n + 1) = 0 := by rw [convergents'_aux, h, convergents'_aux._match_1] +theorem convergents'Aux_succ_none {s : Stream'.Seq (Pair K)} (h : s.head = none) (n : ℕ) : + convergents'Aux s (n + 1) = 0 := by simp [convergents'Aux, h, convergents'Aux.match_1] #align generalized_continued_fraction.convergents'_aux_succ_none GeneralizedContinuedFraction.convergents'Aux_succ_none -theorem convergents'Aux_succ_some {s : Seq (Pair K)} {p : Pair K} (h : s.headI = some p) (n : ℕ) : +theorem convergents'Aux_succ_some {s : Stream'.Seq (Pair K)} {p : Pair K} (h : s.head = some p) (n : ℕ) : convergents'Aux s (n + 1) = p.a / (p.b + convergents'Aux s.tail n) := by - rw [convergents'_aux, h, convergents'_aux._match_1] + simp [convergents'Aux, h, convergents'Aux.match_1] #align generalized_continued_fraction.convergents'_aux_succ_some GeneralizedContinuedFraction.convergents'Aux_succ_some end WithDivisionRing end GeneralizedContinuedFraction + From 0ff912273f96c777b44c57fdcad4e25d6809e7e9 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 3 May 2023 21:19:05 +0200 Subject: [PATCH 6/8] put section back --- Mathlib/Algebra/ContinuedFractions/Translations.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/ContinuedFractions/Translations.lean b/Mathlib/Algebra/ContinuedFractions/Translations.lean index b9fd475568abe..c568d1dcff18e 100644 --- a/Mathlib/Algebra/ContinuedFractions/Translations.lean +++ b/Mathlib/Algebra/ContinuedFractions/Translations.lean @@ -22,9 +22,7 @@ Some simple translation lemmas between the different definitions of functions de namespace GeneralizedContinuedFraction -/- ./././Mathport/Syntax/Translate/Command.lean:229:11: unsupported: unusual advanced open style -/ --- porting note: TODO --- section General +section General /-! ### Translations Between General Access Functions @@ -77,7 +75,7 @@ theorem exists_s_b_of_part_denom {b : α} simpa [partialDenominators, Stream'.Seq.map_get?] using nth_part_denom_eq #align generalized_continued_fraction.exists_s_b_of_part_denom GeneralizedContinuedFraction.exists_s_b_of_part_denom --- end General +end General section WithDivisionRing @@ -192,4 +190,3 @@ theorem convergents'Aux_succ_some {s : Stream'.Seq (Pair K)} {p : Pair K} (h : s end WithDivisionRing end GeneralizedContinuedFraction - From 5c6338c9842a78628ed960fdee209603bae0ca92 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 3 May 2023 21:19:51 +0200 Subject: [PATCH 7/8] manual: comments --- Mathlib/Algebra/ContinuedFractions/Translations.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/ContinuedFractions/Translations.lean b/Mathlib/Algebra/ContinuedFractions/Translations.lean index c568d1dcff18e..0cfeba3022a05 100644 --- a/Mathlib/Algebra/ContinuedFractions/Translations.lean +++ b/Mathlib/Algebra/ContinuedFractions/Translations.lean @@ -16,7 +16,7 @@ import Mathlib.Algebra.ContinuedFractions.Basic ## Summary Some simple translation lemmas between the different definitions of functions defined in -`algebra.continued_fractions.basic`. +`Algebra.ContinuedFractions.Basic`. -/ From 4b58f628ce522a1164795f6ccb975c2137242f91 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 3 May 2023 21:23:42 +0200 Subject: [PATCH 8/8] line length lint --- Mathlib/Algebra/ContinuedFractions/Translations.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/ContinuedFractions/Translations.lean b/Mathlib/Algebra/ContinuedFractions/Translations.lean index 0cfeba3022a05..7d8243cc059ba 100644 --- a/Mathlib/Algebra/ContinuedFractions/Translations.lean +++ b/Mathlib/Algebra/ContinuedFractions/Translations.lean @@ -182,8 +182,8 @@ theorem convergents'Aux_succ_none {s : Stream'.Seq (Pair K)} (h : s.head = none) convergents'Aux s (n + 1) = 0 := by simp [convergents'Aux, h, convergents'Aux.match_1] #align generalized_continued_fraction.convergents'_aux_succ_none GeneralizedContinuedFraction.convergents'Aux_succ_none -theorem convergents'Aux_succ_some {s : Stream'.Seq (Pair K)} {p : Pair K} (h : s.head = some p) (n : ℕ) : - convergents'Aux s (n + 1) = p.a / (p.b + convergents'Aux s.tail n) := by +theorem convergents'Aux_succ_some {s : Stream'.Seq (Pair K)} {p : Pair K} (h : s.head = some p) + (n : ℕ) : convergents'Aux s (n + 1) = p.a / (p.b + convergents'Aux s.tail n) := by simp [convergents'Aux, h, convergents'Aux.match_1] #align generalized_continued_fraction.convergents'_aux_succ_some GeneralizedContinuedFraction.convergents'Aux_succ_some