Commit 2023-05-07 14:02 8e5a00a8

View on Github →

feat: port Algebra.ContinuedFractions.Computation.Translations (#3794)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

added theorem GeneralizedContinuedFraction.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some

added theorem GeneralizedContinuedFraction.IntFractPair.exists_succ_nth_stream_of_fr_zero

added theorem GeneralizedContinuedFraction.IntFractPair.get?_seq1_eq_succ_get?_stream

added theorem GeneralizedContinuedFraction.IntFractPair.seq1_fst_eq_of

added theorem GeneralizedContinuedFraction.IntFractPair.stream_eq_none_of_fr_eq_zero

added theorem GeneralizedContinuedFraction.IntFractPair.stream_succ

added theorem GeneralizedContinuedFraction.IntFractPair.stream_succ_of_int

added theorem GeneralizedContinuedFraction.IntFractPair.stream_succ_of_some

added theorem GeneralizedContinuedFraction.IntFractPair.stream_zero

added theorem GeneralizedContinuedFraction.IntFractPair.succ_nth_stream_eq_none_iff

added theorem GeneralizedContinuedFraction.IntFractPair.succ_nth_stream_eq_some_iff

added theorem GeneralizedContinuedFraction.convergents'_of_int

added theorem GeneralizedContinuedFraction.convergents'_succ

added theorem GeneralizedContinuedFraction.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero

added theorem GeneralizedContinuedFraction.get?_of_eq_some_of_succ_get?_intFractPair_stream

added theorem GeneralizedContinuedFraction.of_h_eq_floor

added theorem GeneralizedContinuedFraction.of_h_eq_intFractPair_seq1_fst_b

added theorem GeneralizedContinuedFraction.of_s_head

added theorem GeneralizedContinuedFraction.of_s_head_aux

added theorem GeneralizedContinuedFraction.of_s_of_int

added theorem GeneralizedContinuedFraction.of_s_succ

added theorem GeneralizedContinuedFraction.of_s_tail

added theorem GeneralizedContinuedFraction.of_terminatedAt_iff_intFractPair_seq1_terminatedAt

added theorem GeneralizedContinuedFraction.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none