Pell

📁 Source: Mathlib/NumberTheory/Pell.lean

Statistics

Metric	Count
Definitions IsFundamental, Solution₁, instCoeZsqrtd, instCommGroup, instHasDistribNeg, instInhabited, mk, x, y	9
Theorems d_nonsquare, d_pos, eq_pow_of_nonneg, eq_zpow_or_neg_zpow, exists_of_not_isSquare, mul_inv_x_lt_x, mul_inv_x_pos, mul_inv_y_nonneg, subsingleton, x_le_x, x_mul_y_le_y_mul_x, x_pos, y_le_y, y_strictMono, zpow_eq_one_iff, zpow_ne_neg_zpow, zpow_y_lt_iff_lt, coe_mk, d_nonsquare_of_one_lt_x, d_pos_of_one_lt_x, eq_one_of_x_eq_one, eq_one_or_neg_one_iff_y_eq_zero, eq_zero_of_d_neg, exists_nontrivial_of_not_isSquare, exists_pos_of_not_isSquare, exists_pos_variant, ext, ext_iff, prop, prop_x, prop_y, sign_y_zpow_eq_sign_of_x_pos_of_y_pos, x_inv, x_mk, x_mul, x_mul_pos, x_ne_zero, x_neg, x_one, x_pow_pos, x_zpow_pos, y_inv, y_mk, y_mul, y_mul_pos, y_ne_zero_of_one_lt_x, y_neg, y_one, y_pow_succ_pos, y_zpow_pos, existsUnique_pos_generator, exists_iff_not_isSquare, exists_of_not_isSquare, is_pell_solution_iff_mem_unitary, pos_generator_iff_fundamental	55
Total	64

Pell

Definitions

Name	Category	Theorems
IsFundamental 📖	MathDef	2 math math: IsFundamental.exists_of_not_isSquare, pos_generator_iff_fundamental
Solution₁ 📖	CompOp	28 math math: Solution₁.y_pow_succ_pos, Solution₁.sign_y_zpow_eq_sign_of_x_pos_of_y_pos, existsUnique_pos_generator, IsFundamental.mul_inv_x_pos, Solution₁.eq_one_or_neg_one_iff_y_eq_zero, IsFundamental.eq_zpow_or_neg_zpow, Solution₁.x_mul, IsFundamental.zpow_eq_one_iff, Solution₁.y_zpow_pos, Solution₁.y_mul_pos, Solution₁.y_neg, IsFundamental.mul_inv_y_nonneg, Solution₁.eq_one_of_x_eq_one, Solution₁.exists_pos_variant, IsFundamental.zpow_y_lt_iff_lt, Solution₁.x_one, Solution₁.y_inv, IsFundamental.mul_inv_x_lt_x, Solution₁.x_mul_pos, Solution₁.x_neg, Solution₁.x_inv, IsFundamental.eq_pow_of_nonneg, pos_generator_iff_fundamental, Solution₁.y_one, Solution₁.y_mul, Solution₁.x_pow_pos, IsFundamental.y_strictMono, Solution₁.x_zpow_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
existsUnique_pos_generator 📖	mathematical	IsSquare	ExistsUnique Solution₁ Solution₁.x Solution₁.y	—	IsFundamental.exists_of_not_isSquare IsFundamental.eq_zpow_or_neg_zpow sub_eq_add_neg zpow_add neg_mul zpow_neg_one mul_inv_eq_one zpow_mul Int.isUnit_iff IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid sub_eq_zero IsFundamental.zpow_eq_one_iff zpow_one lt_irrefl LT.lt.trans neg_zero lt_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Solution₁.y_inv IsFundamental.zpow_ne_neg_zpow zpow_zero Solution₁.x_zpow_pos zero_lt_one Int.instZeroLEOneClass Solution₁.x_neg Mathlib.Meta.NormNum.isInt_lt_false IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg
exists_iff_not_isSquare 📖	mathematical	—	Monoid.toNatPow Int.instMonoid IsSquare	—	sub_eq_add_neg AddLeftCancelSemigroup.toIsLeftCancelAdd IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Int.instCharZero mul_self_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Int.instAddLeftMono contravariant_lt_of_covariant_le Int.eq_of_mul_eq_one sq_sub_sq mul_pow sq exists_of_not_isSquare
exists_of_not_isSquare 📖	mathematical	IsSquare	Monoid.toNatPow Int.instMonoid	—	irrational_nrt_of_notint_nrt Real.sq_sqrt Int.cast_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass LT.lt.le Int.cast_injective IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Int.cast_mul sq two_pos Nat.instZeroLEOneClass Nat.instIsOrderedAddMonoid Nat.instAtLeastTwoHAddOfNat exists_int_gt Real.instArchimedean Set.Infinite.mono pow_pos IsStrictOrderedRing.toPosMulStrictMono Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Rat.pos Int.cast_natCast Rat.instCharZero Rat.num_div_den Set.mem_setOf abs_sub_comm Int.cast_lt NeZero.charZero_one div_lt_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono abs_pos_of_pos Int.cast_abs Int.cast_sub Int.cast_pow abs_div abs_sq sub_div mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass LT.lt.ne' div_pow Int.cast_pos sq_sub_sq abs_mul mul_one_div mul_lt_mul'' IsOrderedRing.toMulPosMono LE.le.trans_lt LE.le.trans abs_add_le two_mul add_assoc add_le_add_iff_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le sub_le_iff_le_add' abs_sub_abs_le_abs_sub div_le_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE one_le_sq_iff_one_le_abs Nat.abs_cast Nat.one_le_cast abs_nonneg covariant_swap_add_of_covariant_add Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational Mathlib.Tactic.Contrapose.contrapose₁ Set.ext Set.iUnion_congr_Prop Int.instAddLeftMono Set.Finite.biUnion Set.finite_Ioo Set.Infinite.nonempty two_ne_zero mul_comm sub_eq_zero mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero Int.instIsCancelMulZero Int.instIsStrictOrderedRing Int.instZeroLEOneClass mul_pow Set.Infinite.exists_ne_map_eq_of_mapsTo Set.mapsTo_univ Set.finite_univ Finite.instProd Finite.of_fintype ZMod.intCast_zmod_eq_zero_iff_dvd Nat.cast_zero Nat.cast_pow Int.cast_zero dvd_refl ZMod.intCast_eq_intCast_iff_dvd_sub Int.cast_ne_zero Int.cast_div_charZero Int.cast_one Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.pow_eq_eval 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.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial div_ne_zero_iff Rat.eq_iff_mul_eq_mul
is_pell_solution_iff_mem_unitary 📖	mathematical	—	Monoid.toNatPow Int.instMonoid Zsqrtd.re Zsqrtd.im Zsqrtd Submonoid Monoid.toMulOneClass Zsqrtd.instMonoid SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CommSemiring.toSemiring CommRing.toCommSemiring Zsqrtd.commRing Zsqrtd.instStarRing	—	Zsqrtd.norm_eq_one_iff_mem_unitary Zsqrtd.norm_def sq mul_assoc
pos_generator_iff_fundamental 📖	mathematical	—	Solution₁.x Solution₁.y Solution₁ DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup Solution₁.instCommGroup InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Solution₁.instHasDistribNeg IsFundamental	—	Solution₁.d_pos_of_one_lt_x Solution₁.d_nonsquare_of_one_lt_x IsFundamental.exists_of_not_isSquare existsUnique_pos_generator IsFundamental.eq_zpow_or_neg_zpow

Pell.IsFundamental

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_nonsquare 📖	mathematical	Pell.IsFundamental	IsSquare	—	Pell.Solution₁.d_nonsquare_of_one_lt_x
d_pos 📖	—	Pell.IsFundamental	—	—	Pell.Solution₁.d_pos_of_one_lt_x
eq_pow_of_nonneg 📖	mathematical	Pell.IsFundamental Pell.Solution₁.x Pell.Solution₁.y	Pell.Solution₁ Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Pell.Solution₁.instCommGroup	—	CanLift.prf instCanLiftIntNatCastLeOfNat LT.lt.le Nat.strong_induction_on LE.le.eq_or_lt pow_zero Pell.Solution₁.ext Pell.Solution₁.prop sq_eq_one_iff IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE sub_zero MulZeroClass.mul_zero MulZeroClass.zero_mul sq LE.le.trans_eq LT.lt.trans_eq Mathlib.Meta.NormNum.isInt_le_false IsStrictOrderedRing.toIsOrderedRing Int.instNontrivial Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_add 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.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le neg_eq_zero mul_nonneg_of_nonpos_of_nonpos IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add Int.instAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le sq_nonneg IsOrderedRing.toPosMulMono d_pos Mathlib.Tactic.Linarith.mul_zero_eq Mathlib.Tactic.Linarith.natCast_nonneg Mathlib.Tactic.Linarith.zero_mul_eq mul_inv_x_pos mul_inv_x_lt_x mul_inv_y_nonneg Int.instZeroLEOneClass Int.instCharZero pow_succ' mul_comm mul_assoc mul_inv_cancel one_mul
eq_zpow_or_neg_zpow 📖	mathematical	Pell.IsFundamental	Pell.Solution₁ DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup Pell.Solution₁.instCommGroup InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Pell.Solution₁.instHasDistribNeg	—	Pell.Solution₁.exists_pos_variant d_pos eq_pow_of_nonneg zpow_natCast zpow_neg Set.mem_singleton_iff
exists_of_not_isSquare 📖	mathematical	IsSquare	Pell.IsFundamental	—	Pell.Solution₁.exists_pos_of_not_isSquare Pell.Solution₁.prop CanLift.prf instCanLiftIntNatCastLeOfNat le_of_lt lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero Nat.find_spec Nat.cast_zero Nat.find.congr_simp LE.le.trans zero_le_one LT.lt.le Nat.find_min' abs_pos Pell.Solution₁.y_ne_zero_of_one_lt_x sq_abs
mul_inv_x_lt_x 📖	mathematical	Pell.IsFundamental Pell.Solution₁.x Pell.Solution₁.y	Pell.Solution₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Pell.Solution₁.instCommGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	Pell.Solution₁.x_mul mul_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono lt_of_mul_lt_mul_left PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Int.instIsStrictOrderedRing Mathlib.Tactic.Ring.of_eq 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 x_mul_y_le_y_mul_x mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing le_of_lt lt_trans Mathlib.Meta.Positivity.pos_of_isNat Int.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat mul_assoc sq Pell.Solution₁.prop_x sub_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add abs_of_pos LT.lt.trans zero_lt_one Int.instZeroLEOneClass abs_mul sq_lt_sq mul_pow one_mul mul_le_mul_iff_left₀ MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono sq_pos_of_pos d_pos lt_add_one add_comm mul_one mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono add_pos' mul_pos pow_pos IsStrictOrderedRing.toZeroLEOneClass Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw 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.Tactic.Ring.neg_zero 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 LT.lt.le
mul_inv_x_pos 📖	mathematical	Pell.IsFundamental Pell.Solution₁.x Pell.Solution₁.y	Pell.Solution₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Pell.Solution₁.instCommGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	Pell.Solution₁.x_mul mul_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.instAddLeftMono zero_add lt_of_mul_lt_mul_left PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Int.instIsStrictOrderedRing Mathlib.Tactic.Ring.of_eq 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 x_mul_y_le_y_mul_x d_pos mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing le_of_lt mul_pos Pell.Solution₁.prop_y Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true Int.instCharZero Mathlib.Tactic.Linarith.sub_nonpos_of_le LE.le.trans zero_le_one Int.instZeroLEOneClass LT.lt.le
mul_inv_y_nonneg 📖	mathematical	Pell.IsFundamental Pell.Solution₁.x Pell.Solution₁.y	Pell.Solution₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Pell.Solution₁.instCommGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	mul_neg Int.instAddLeftMono add_zero x_mul_y_le_y_mul_x
subsingleton 📖	—	Pell.IsFundamental	—	—	le_antisymm Pell.Solution₁.ext Pell.Solution₁.prop_y sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Int.instIsStrictOrderedRing IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing LT.lt.le LT.lt.ne' d_pos
x_le_x 📖	—	Pell.IsFundamental Pell.Solution₁.x	—	—	—
x_mul_y_le_y_mul_x 📖	—	Pell.IsFundamental Pell.Solution₁.x Pell.Solution₁.y	—	—	abs_of_pos Int.instAddLeftMono LT.lt.trans zero_lt_one Int.instZeroLEOneClass x_pos abs_mul IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing sq_le_sq mul_pow Pell.Solution₁.prop_x sub_nonneg covariant_swap_add_of_covariant_add Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.RingNF.nat_rawCast_1 mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg add_zero Mathlib.Tactic.RingNF.add_neg y_le_y
x_pos 📖	mathematical	Pell.IsFundamental	Pell.Solution₁.x	—	LT.lt.trans zero_lt_one Int.instZeroLEOneClass
y_le_y 📖	—	Pell.IsFundamental Pell.Solution₁.x Pell.Solution₁.y	—	—	Pell.Solution₁.prop_x Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add abs_of_pos Int.instAddLeftMono sq_le_sq Int.instIsStrictOrderedRing mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono d_pos sub_nonpos covariant_swap_add_of_covariant_add mul_sub LT.lt.trans zero_lt_one Int.instZeroLEOneClass x_le_x
y_strictMono 📖	mathematical	Pell.IsFundamental	StrictMono PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder Pell.Solution₁.y Pell.Solution₁ DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup Pell.Solution₁.instCommGroup	—	sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.instAddLeftMono zpow_add zpow_one Pell.Solution₁.y_mul add_sub_assoc Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_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.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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add add_pos_of_pos_of_nonneg mul_pos IsStrictOrderedRing.toPosMulStrictMono Int.instIsStrictOrderedRing Pell.Solution₁.x_zpow_pos x_pos mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing LE.le.eq_or_lt zpow_zero LT.lt.le Pell.Solution₁.y_zpow_pos sub_nonneg strictMono_int_of_lt_succ le_or_gt neg_sub sub_neg_eq_add add_tsub_cancel_left AddGroup.toOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le sub_add_cancel neg_add' zpow_neg Pell.Solution₁.y_inv neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
zpow_eq_one_iff 📖	mathematical	Pell.IsFundamental	Pell.Solution₁ DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup Pell.Solution₁.instCommGroup InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	zpow_zero StrictMono.injective y_strictMono
zpow_ne_neg_zpow 📖	—	Pell.IsFundamental	—	—	Pell.Solution₁.x_zpow_pos x_pos lt_irrefl LT.lt.trans neg_zero lt_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Pell.Solution₁.x_neg
zpow_y_lt_iff_lt 📖	mathematical	Pell.IsFundamental	Pell.Solution₁.y Pell.Solution₁ DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup Pell.Solution₁.instCommGroup	—	Mathlib.Tactic.Contrapose.contrapose₁ StrictMono.monotone y_strictMono

Pell.Solution₁

Definitions

Name	Category	Theorems
instCoeZsqrtd 📖	CompOp	—
instCommGroup 📖	CompOp	27 math math: y_pow_succ_pos, sign_y_zpow_eq_sign_of_x_pos_of_y_pos, Pell.IsFundamental.mul_inv_x_pos, eq_one_or_neg_one_iff_y_eq_zero, Pell.IsFundamental.eq_zpow_or_neg_zpow, x_mul, Pell.IsFundamental.zpow_eq_one_iff, y_zpow_pos, y_mul_pos, y_neg, Pell.IsFundamental.mul_inv_y_nonneg, eq_one_of_x_eq_one, exists_pos_variant, Pell.IsFundamental.zpow_y_lt_iff_lt, x_one, y_inv, Pell.IsFundamental.mul_inv_x_lt_x, x_mul_pos, x_neg, x_inv, Pell.IsFundamental.eq_pow_of_nonneg, Pell.pos_generator_iff_fundamental, y_one, y_mul, x_pow_pos, Pell.IsFundamental.y_strictMono, x_zpow_pos
instHasDistribNeg 📖	CompOp	6 math math: eq_one_or_neg_one_iff_y_eq_zero, Pell.IsFundamental.eq_zpow_or_neg_zpow, y_neg, exists_pos_variant, x_neg, Pell.pos_generator_iff_fundamental
instInhabited 📖	CompOp	—
mk 📖	CompOp	—
x 📖	CompOp	16 math math: Pell.existsUnique_pos_generator, x_mul, exists_pos_variant, prop_y, prop, x_one, exists_pos_of_not_isSquare, x_neg, eq_zero_of_d_neg, x_inv, Pell.pos_generator_iff_fundamental, Pell.IsFundamental.x_pos, prop_x, y_mul, x_mk, ext_iff
y 📖	CompOp	18 math math: Pell.existsUnique_pos_generator, eq_one_or_neg_one_iff_y_eq_zero, x_mul, y_neg, exists_pos_variant, prop_y, Pell.IsFundamental.zpow_y_lt_iff_lt, prop, exists_pos_of_not_isSquare, y_inv, eq_zero_of_d_neg, Pell.pos_generator_iff_fundamental, prop_x, y_one, y_mk, y_mul, Pell.IsFundamental.y_strictMono, ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mk 📖	mathematical	Monoid.toNatPow Int.instMonoid	Zsqrtd Submonoid Monoid.toMulOneClass Zsqrtd.instMonoid SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CommSemiring.toSemiring CommRing.toCommSemiring Zsqrtd.commRing Zsqrtd.instStarRing	—	Zsqrtd.ext
d_nonsquare_of_one_lt_x 📖	mathematical	x	IsSquare	—	prop sq_sub_sq
d_pos_of_one_lt_x 📖	—	x	—	—	pos_of_mul_pos_left MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Int.instIsStrictOrderedRing prop_y sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.instAddLeftMono one_lt_pow₀ Int.instZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing two_ne_zero sq_nonneg AddGroup.existsAddOfLE
eq_one_of_x_eq_one 📖	mathematical	x	Pell.Solution₁ InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup	—	prop_y ext sq_eq_zero_iff isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE mul_eq_zero sub_self one_pow
eq_one_or_neg_one_iff_y_eq_zero 📖	mathematical	—	Pell.Solution₁ InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instHasDistribNeg y	—	neg_zero prop ext sq_eq_one_iff IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE sub_zero MulZeroClass.mul_zero sq
eq_zero_of_d_neg 📖	mathematical	—	x y	—	prop Mathlib.Tactic.Contrapose.contrapose₁ sq_pos_of_ne_zero Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add 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.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.lt_of_lt_of_eq neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing sub_eq_zero_of_eq mul_nonneg_of_nonpos_of_nonpos IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add Int.instAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le sq_nonneg IsOrderedRing.toPosMulMono
exists_nontrivial_of_not_isSquare 📖	—	IsSquare	—	—	Pell.exists_of_not_isSquare neg_zero
exists_pos_of_not_isSquare 📖	mathematical	IsSquare	x y	—	Pell.exists_of_not_isSquare sq_abs one_lt_sq_iff_one_lt_abs Int.instIsStrictOrderedRing eq_add_of_sub_eq lt_add_iff_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono contravariant_lt_of_covariant_le mul_pos IsStrictOrderedRing.toPosMulStrictMono sq_pos_of_ne_zero AddGroup.existsAddOfLE abs_pos
exists_pos_variant 📖	mathematical	—	x y Pell.Solution₁ Set Set.instMembership Set.instInsert InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instHasDistribNeg Set.instSingletonSet	—	lt_or_gt_of_ne x_ne_zero LT.lt.le le_total neg_inv IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono neg_neg inv_inv
ext 📖	—	x y	—	—	Zsqrtd.ext
ext_iff 📖	mathematical	—	x y	—	ext
prop 📖	mathematical	—	Monoid.toNatPow Int.instMonoid x y	—	Pell.is_pell_solution_iff_mem_unitary
prop_x 📖	mathematical	—	Monoid.toNatPow Int.instMonoid x y	—	prop Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right 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_lt Mathlib.Tactic.Ring.add_pf_zero_add 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
prop_y 📖	mathematical	—	Monoid.toNatPow Int.instMonoid y x	—	prop Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add
sign_y_zpow_eq_sign_of_x_pos_of_y_pos 📖	mathematical	x y	Pell.Solution₁ DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	zpow_natCast y_pow_succ_pos zpow_negSucc neg_neg_of_pos Int.instIsOrderedAddMonoid
x_inv 📖	mathematical	—	x Pell.Solution₁ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup	—	—
x_mk 📖	mathematical	Monoid.toNatPow Int.instMonoid	x	—	—
x_mul 📖	mathematical	—	x Pell.Solution₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup y	—	mul_assoc
x_mul_pos 📖	mathematical	x	Pell.Solution₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	x_mul neg_lt_iff_pos_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono abs_lt covariant_swap_add_of_covariant_add abs_of_pos abs_mul IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing sq_lt_sq mul_pow prop_x sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt 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.Tactic.Ring.neg_zero 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 Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.RingNF.add_assoc_rev le_or_gt add_pos_of_pos_of_nonneg Mathlib.Meta.Positivity.pos_of_isNat Int.instNontrivial mul_nonneg IsOrderedRing.toPosMulMono Even.pow_nonneg AddGroup.existsAddOfLE even_two_mul eq_zero_of_d_neg LT.lt.ne' zero_pow Nat.instCharZero MulZeroClass.mul_zero Int.instZeroLEOneClass
x_ne_zero 📖	—	—	—	—	mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing sq_nonneg AddGroup.existsAddOfLE Int.instAddLeftMono not_le neg_one_lt_zero Int.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd zero_sub MulZeroClass.zero_mul sq prop_y
x_neg 📖	mathematical	—	x Pell.Solution₁ InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup instHasDistribNeg	—	—
x_one 📖	mathematical	—	x Pell.Solution₁ InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup	—	—
x_pow_pos 📖	mathematical	x	Pell.Solution₁ Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	pow_zero Int.instZeroLEOneClass pow_succ x_mul_pos
x_zpow_pos 📖	mathematical	x	Pell.Solution₁ DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	zpow_natCast x_pow_pos zpow_negSucc
y_inv 📖	mathematical	—	y Pell.Solution₁ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup	—	—
y_mk 📖	mathematical	Monoid.toNatPow Int.instMonoid	y	—	—
y_mul 📖	mathematical	—	y Pell.Solution₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup x	—	—
y_mul_pos 📖	mathematical	x y	Pell.Solution₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	add_pos' Int.instAddLeftMono mul_pos IsStrictOrderedRing.toPosMulStrictMono Int.instIsStrictOrderedRing
y_ne_zero_of_one_lt_x 📖	—	x	—	—	prop lt_irrefl LT.lt.trans_eq one_lt_sq_iff₀ IsStrictOrderedRing.toPosMulStrictMono Int.instIsStrictOrderedRing Int.instZeroLEOneClass LE.le.trans zero_le_one LT.lt.le sub_zero MulZeroClass.mul_zero MulZeroClass.zero_mul sq
y_neg 📖	mathematical	—	y Pell.Solution₁ InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup instHasDistribNeg	—	—
y_one 📖	mathematical	—	y Pell.Solution₁ InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instCommGroup	—	—
y_pow_succ_pos 📖	mathematical	x y	Pell.Solution₁ Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	pow_one pow_succ' y_mul_pos x_pow_pos
y_zpow_pos 📖	mathematical	x y	Pell.Solution₁ DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup instCommGroup	—	CanLift.prf instCanLiftIntNatCastLeOfNat LT.lt.le Nat.cast_zero zpow_natCast Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero y_pow_succ_pos

---

← Back to Index