Translations

📁 Source: Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_succ_get?_stream_of_gcf_of_get?_eq_some, exists_succ_nth_stream_of_fr_zero, get?_seq1_eq_succ_get?_stream, seq1_fst_eq_of, stream_eq_none_of_fr_eq_zero, stream_succ, stream_succ_of_int, stream_succ_of_some, stream_zero, succ_nth_stream_eq_none_iff, succ_nth_stream_eq_some_iff, convs'_of_int, convs'_succ, get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero, get?_of_eq_some_of_succ_get?_intFractPair_stream, of_h_eq_floor, of_h_eq_intFractPair_seq1_fst_b, of_s_head, of_s_head_aux, of_s_of_int, of_s_succ, of_s_tail, of_terminatedAt_iff_intFractPair_seq1_terminatedAt, of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none	24
Total	24

GenContFract

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convs'_of_int 📖	mathematical	—	convs' of AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing	—	zeroth_conv'_eq_h of_h_eq_floor Int.floor_intCast convs'.eq_1 add_eq_left AddLeftCancelSemigroup.toIsLeftCancelAdd convs'Aux_succ_none Stream'.Seq.get?_nil of_s_of_int
convs'_succ 📖	mathematical	—	convs' of Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.floor DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring Int.fract	—	eq_or_ne eq_of_sub_eq_zero convs'_of_int Int.fract_intCast inv_zero Int.cast_zero div_zero add_zero Int.floor_intCast convs'.eq_1 of_h_eq_floor AddLeftCancelSemigroup.toIsLeftCancelAdd convs'Aux_succ_some of_s_head of_s_tail
get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero 📖	mathematical	IntFractPair.stream IntFractPair	Stream'.Seq.get? Pair s of AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing AddGroupWithOne.toIntCast IntFractPair.b IntFractPair.of InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring IntFractPair.fr	—	get?_of_eq_some_of_succ_get?_intFractPair_stream IntFractPair.stream_succ_of_some
get?_of_eq_some_of_succ_get?_intFractPair_stream 📖	mathematical	IntFractPair.stream IntFractPair	Stream'.Seq.get? Pair s of AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing AddGroupWithOne.toIntCast IntFractPair.b	—	IntFractPair.stream_isSeq Stream'.Seq.map_tail Stream'.Seq.map_get?
of_h_eq_floor 📖	mathematical	—	h of AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Int.floor	—	of_h_eq_intFractPair_seq1_fst_b
of_h_eq_intFractPair_seq1_fst_b 📖	mathematical	—	h of AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing IntFractPair.b IntFractPair Stream'.Seq IntFractPair.seq1	—	—
of_s_head 📖	mathematical	—	Stream'.Seq.head Pair s of AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing AddGroupWithOne.toIntCast Int.floor InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring Int.fract	—	of_s_head_aux IntFractPair.stream_succ_of_some IntFractPair.stream_zero
of_s_head_aux 📖	mathematical	—	Stream'.Seq.get? Pair s of IntFractPair IntFractPair.stream AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing AddGroupWithOne.toIntCast IntFractPair.b	—	of.eq_1 IntFractPair.stream_isSeq IntFractPair.seq1.eq_1 Stream'.get_succ Stream'.get.eq_1 Option.bind_congr'
of_s_of_int 📖	mathematical	—	s of AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Stream'.Seq.nil Pair	—	Stream'.Seq.ext of_s_head_aux IntFractPair.stream_succ_of_int Subtype.prop Stream'.Seq.get?_nil
of_s_succ 📖	mathematical	—	Stream'.Seq.get? Pair s of InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring Int.fract DivisionRing.toRing	—	eq_or_ne eq_of_sub_eq_zero Int.fract_intCast inv_zero of_s_of_int Int.cast_zero Stream'.Seq.get?_nil terminatedAt_iff_s_none of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none IntFractPair.stream_succ IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some get?_of_eq_some_of_succ_get?_intFractPair_stream
of_s_tail 📖	mathematical	—	Stream'.Seq.tail Pair s of InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring Int.fract DivisionRing.toRing	—	Stream'.Seq.ext of_s_succ Stream'.Seq.get?_tail
of_terminatedAt_iff_intFractPair_seq1_terminatedAt 📖	mathematical	—	TerminatedAt of Stream'.Seq.TerminatedAt IntFractPair Stream'.Seq IntFractPair.seq1	—	IntFractPair.stream_isSeq
of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none 📖	mathematical	—	TerminatedAt of IntFractPair.stream IntFractPair	—	of_terminatedAt_iff_intFractPair_seq1_terminatedAt Stream'.Seq.TerminatedAt.eq_1 IntFractPair.get?_seq1_eq_succ_get?_stream

GenContFract.IntFractPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_succ_get?_stream_of_gcf_of_get?_eq_some 📖	mathematical	Stream'.Seq.get? GenContFract.Pair GenContFract.s GenContFract.of	stream GenContFract.IntFractPair AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing b GenContFract.Pair.b	—	stream_isSeq Stream'.Seq.map_tail Stream'.Seq.map_get?
exists_succ_nth_stream_of_fr_zero 📖	mathematical	stream GenContFract.IntFractPair fr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Int.floor	—	succ_nth_stream_eq_some_iff
get?_seq1_eq_succ_get?_stream 📖	mathematical	—	Stream'.Seq.get? GenContFract.IntFractPair Stream'.Seq seq1 stream	—	—
seq1_fst_eq_of 📖	mathematical	—	GenContFract.IntFractPair Stream'.Seq seq1 of	—	—
stream_eq_none_of_fr_eq_zero 📖	—	stream GenContFract.IntFractPair fr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing	—	—	Option.bind_congr'
stream_succ 📖	mathematical	—	stream InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring Int.fract DivisionRing.toRing	—	stream_zero stream_succ_of_some ne_of_eq_of_ne eq_or_ne succ_nth_stream_eq_none_iff stream_eq_none_of_fr_eq_zero
stream_succ_of_int 📖	mathematical	—	stream AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing GenContFract.IntFractPair	—	stream_eq_none_of_fr_eq_zero stream_zero Int.fract_intCast succ_nth_stream_eq_none_iff
stream_succ_of_some 📖	mathematical	stream GenContFract.IntFractPair	of InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring fr	—	succ_nth_stream_eq_some_iff
stream_zero 📖	mathematical	—	stream GenContFract.IntFractPair of	—	—
succ_nth_stream_eq_none_iff 📖	mathematical	—	stream GenContFract.IntFractPair fr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing	—	stream.eq_2
succ_nth_stream_eq_some_iff 📖	mathematical	—	stream GenContFract.IntFractPair of InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring fr	—	—

---

← Back to Index