CorrectnessTerminating

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

Statistics

Metric	Count
Definitions compExactValue	1
Theorems compExactValue_correctness_of_stream_eq_some, compExactValue_correctness_of_stream_eq_some_aux_comp, of_correctness_atTop_of_terminates, of_correctness_of_nth_stream_eq_none, of_correctness_of_terminatedAt, of_correctness_of_terminates	6
Total	7

GenContFract

Definitions

Name	Category	Theorems
compExactValue 📖	CompOp	1 math math: compExactValue_correctness_of_stream_eq_some

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compExactValue_correctness_of_stream_eq_some 📖	mathematical	IntFractPair.stream Field.toDivisionRing IntFractPair	compExactValue contsAux of IntFractPair.fr	—	eq_or_ne Int.fract_add_floor zero_add of_h_eq_floor div_one mul_one MulZeroClass.mul_zero add_zero div_inv_eq_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Int.floor_add_fract IntFractPair.succ_nth_stream_eq_some_iff IntFractPair.exists_succ_nth_stream_of_fr_zero get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero Semigroup.to_isAssociative CommMagma.to_isCommutative AddSemigroup.to_isAssociative AddCommMagma.to_isCommutative compExactValue_correctness_of_stream_eq_some_aux_comp one_div contsAux_recurrence
compExactValue_correctness_of_stream_eq_some_aux_comp 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Distrib.toMul AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Int.floor Int.fract	—	Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Int.fract.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
of_correctness_atTop_of_terminates 📖	mathematical	Terminates of Field.toDivisionRing	Filter.Eventually convs Filter.atTop Nat.instPreorder	—	Filter.eventually_atTop SemilatticeSup.instIsDirectedOrder convs_stable_of_terminated of_correctness_of_terminatedAt
of_correctness_of_nth_stream_eq_none 📖	mathematical	IntFractPair.stream Field.toDivisionRing IntFractPair	convs of	—	IntFractPair.succ_nth_stream_eq_none_iff of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none convs_stable_of_terminated compExactValue_correctness_of_stream_eq_some
of_correctness_of_terminatedAt 📖	mathematical	TerminatedAt of Field.toDivisionRing	convs	—	of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none of_correctness_of_nth_stream_eq_none
of_correctness_of_terminates 📖	mathematical	Terminates of Field.toDivisionRing	convs	—	of_correctness_of_terminatedAt

---

← Back to Index