PellMatiyasevic

📁 Source: Mathlib/NumberTheory/PellMatiyasevic.lean

Statistics

Metric	Count
Definitions IsPell, az, pell, pellZd, xn, xz, yn, yz	8
Theorems asq_pos, d_pos, dnsq, dvd_of_ysq_dvd, dz_val, eq_of_xn_modEq, eq_of_xn_modEq', eq_of_xn_modEq_le, eq_of_xn_modEq_lem1, eq_of_xn_modEq_lem2, eq_of_xn_modEq_lem3, eq_pell, eq_pellZd, eq_pell_lem, eq_pow_of_pell, eq_pow_of_pell_lem, im_pellZd, isPell_iff_mem_unitary, isPell_mul, isPell_nat, isPell_norm, isPell_one, isPell_pellZd, isPell_star, matiyasevic, modEq_of_xn_modEq, n_lt_xn, pellZd_add, pellZd_im, pellZd_re, pellZd_sub, pellZd_succ, pellZd_succ_succ, pell_eq, pell_eqz, pell_val, re_pellZd, strictMono_x, strictMono_y, x_pos, x_sub_y_dvd_pow, x_sub_y_dvd_pow_lem, xn_add, xn_ge_a_pow, xn_modEq_x2n_add, xn_modEq_x2n_add_lem, xn_modEq_x2n_sub, xn_modEq_x2n_sub_lem, xn_modEq_x4n_add, xn_modEq_x4n_sub, xn_one, xn_succ, xn_succ_succ, xn_zero, xy_coprime, xy_modEq_of_modEq, xy_modEq_yn, xy_succ_succ, xz_sub, xz_succ, xz_succ_succ, y_dvd_iff, y_mul_dvd, yn_add, yn_ge_n, yn_modEq_a_sub_one, yn_modEq_two, yn_one, yn_succ, yn_succ_succ, yn_zero, ysq_dvd_yy, yz_sub, yz_succ, yz_succ_succ	75
Total	83

Pell

Definitions

Name	Category	Theorems
IsPell 📖	MathDef	6 math math: isPell_norm, isPell_iff_mem_unitary, isPell_nat, isPell_star, isPell_pellZd, isPell_one
az 📖	CompOp	3 math math: dz_val, xz_succ, yz_succ
pell 📖	CompOp	1 math math: pell_val
pellZd 📖	CompOp	10 math math: pellZd_sub, eq_pellZd, pellZd_succ, pellZd_succ_succ, re_pellZd, pellZd_re, pellZd_add, im_pellZd, isPell_pellZd, pellZd_im
xn 📖	CompOp	32 math math: eq_of_xn_modEq_lem3, xy_succ_succ, xn_modEq_x4n_add, eq_pell, yn_add, xn_succ, Dioph.xn_dioph, x_pos, xy_modEq_yn, xy_coprime, yn_succ, n_lt_xn, re_pellZd, xn_modEq_x2n_sub, xy_modEq_of_modEq, matiyasevic, pell_val, xn_modEq_x2n_add, pellZd_re, strictMono_x, xn_modEq_x2n_add_lem, xn_add, xn_succ_succ, Dioph.pell_dioph, xn_modEq_x4n_sub, xn_one, xn_zero, pell_eq, xn_modEq_x2n_sub_lem, eq_pow_of_pell, eq_of_xn_modEq_lem1, xn_ge_a_pow
xz 📖	CompOp	7 math math: yz_sub, xz_sub, pell_eqz, xz_succ, x_sub_y_dvd_pow, xz_succ_succ, yz_succ
yn 📖	CompOp	27 math math: ysq_dvd_yy, xy_succ_succ, yn_ge_n, eq_pell, yn_add, xn_succ, strictMono_y, xy_modEq_yn, xy_coprime, yn_zero, yn_succ, xy_modEq_of_modEq, matiyasevic, pell_val, y_dvd_iff, y_mul_dvd, xn_modEq_x2n_add_lem, xn_add, yn_one, Dioph.pell_dioph, yn_modEq_two, im_pellZd, pell_eq, pellZd_im, yn_modEq_a_sub_one, eq_pow_of_pell, yn_succ_succ
yz 📖	CompOp	7 math math: yz_sub, xz_sub, yz_succ_succ, pell_eqz, xz_succ, x_sub_y_dvd_pow, yz_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asq_pos 📖	—	—	—	—	le_trans le_of_lt mul_one
d_pos 📖	—	—	—	—	tsub_pos_of_lt Nat.instCanonicallyOrderedAdd Nat.instOrderedSub mul_lt_mul IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing IsStrictOrderedRing.toMulPosStrictMono le_of_lt
dnsq 📖	mathematical	—	Zsqrtd.Nonsquare	—	asq_pos Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left d_pos LE.le.trans
dvd_of_ysq_dvd 📖	—	yn	—	—	y_dvd_iff dvd_of_mul_left_dvd strictMono_y Nat.modEq_zero_iff_dvd xy_modEq_yn Nat.ModEq.trans Nat.ModEq.symm Nat.ModEq.of_dvd pow_succ pow_zero one_mul Dvd.dvd.modEq_zero_nat dvd_mul_of_dvd_right xy_coprime
dz_val 📖	mathematical	—	az	—	asq_pos
eq_of_xn_modEq 📖	—	Nat.ModEq xn	—	—	le_total eq_of_xn_modEq_le Nat.ModEq.symm
eq_of_xn_modEq' 📖	—	Nat.ModEq xn	—	—	le_trans Nat.instAtLeastTwoHAddOfNat two_mul eq_of_xn_modEq ne_of_gt Nat.ModEq.trans Nat.ModEq.symm xn_modEq_x4n_sub tsub_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le add_tsub_cancel_of_le le_or_gt
eq_of_xn_modEq_le 📖	—	Nat.ModEq xn	—	—	MulZeroClass.mul_zero Nat.instCanonicallyOrderedAdd lt_or_eq_of_le ne_of_gt strictMono_x LT.lt.trans eq_of_xn_modEq_lem3 le_trans ne_of_lt
eq_of_xn_modEq_lem1 📖	mathematical	—	xn	—	strictMono_x lt_or_eq_of_le lt_trans le_of_lt
eq_of_xn_modEq_lem2 📖	—	xn	—	—	ne_of_lt lt_of_le_of_lt mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono d_pos strictMono_y mul_comm xn_succ one_mul MulZeroClass.mul_zero add_zero
eq_of_xn_modEq_lem3 📖	mathematical	—	xn	—	le_of_lt strictMono_x x_pos Nat.ModEq.add_right_cancel' tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub xn_modEq_x2n_sub_lem LT.lt.le Nat.ModEq.trans tsub_tsub_cancel_of_le IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Dvd.dvd.zero_modEq_nat dvd_rfl lt_trichotomy eq_of_xn_modEq_lem1 lt_of_le_of_ne Int.lt_of_ofNat_lt_ofNat Nat.instAtLeastTwoHAddOfNat two_mul tsub_add_eq_tsub_tsub add_tsub_cancel_right lt_sub_left_of_add_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Int.instAddLeftMono Int.ofNat_lt_ofNat_of_lt lt_or_eq_of_le mul_comm xn_succ le_trans lt_of_lt_of_le eq_of_xn_modEq_lem2 le_antisymm tsub_eq_zero_iff_le add_zero LT.lt.ne' lt_trans ne_of_gt sub_lt_sub_left IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add tsub_pos_of_lt
eq_pell 📖	mathematical	—	xn yn	—	zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Zsqrtd.le_of_le_le Int.ofNat_le_ofNat_of_le eq_pellZd isPell_nat
eq_pellZd 📖	mathematical	Zsqrtd Zsqrtd.instLECastInt Zsqrtd.instOne IsPell	pellZd	—	Zsqrtd.le_arch eq_pell_lem LE.le.trans Zsqrtd.natCast_val Zsqrtd.le_of_le_le Int.ofNat_le_ofNat_of_le le_of_lt n_lt_xn
eq_pell_lem 📖	—	Zsqrtd Zsqrtd.instLECastInt Zsqrtd.instOne IsPell pellZd	—	—	Zsqrtd.le_antisymm dnsq zero_add mul_one add_zero one_mul isPell_norm isPell_one mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing Zsqrtd.instIsStrictOrderedRingCastInt isPell_mul isPell_star mul_assoc pellZd_succ mul_comm sub_lt_sub IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Zsqrtd.instIsOrderedAddMonoidCastInt mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono le_trans zero_le_one Zsqrtd.instZeroLEOneClassCastInt sub_self sub_neg_eq_add add_neg_cancel neg_neg le_refl Zsqrtd.le_of_le_le Int.ofNat_le_ofNat_of_le add_le_add Int.instAddLeftMono covariant_swap_add_of_covariant_add lt_or_eq_of_le
eq_pow_of_pell 📖	mathematical	—	Monoid.toNatPow Nat.instMonoid Nat.ModEq xn yn	—	zero_pow LT.lt.ne' le_max_left le_max_right LT.lt.trans_le strictMono_x LE.le.trans LT.lt.le n_lt_xn Nat.modEq_zero_iff_dvd Nat.ModEq.trans yn_modEq_a_sub_one Dvd.dvd.modEq_zero_nat dvd_rfl eq_pow_of_pell_lem xn_ge_a_pow CanLift.prf instCanLiftIntNatCastLeOfNat Nat.cast_nonneg IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Nat.modEq_of_dvd x_sub_y_dvd_pow Nat.instAtLeastTwoHAddOfNat Nat.cast_mul Nat.cast_add Nat.cast_one pell_eq Nat.cast_lt Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero pow_zero eq_pell lt_irrefl Nat.ModEq.symm le_trans sub_sub eq_sub_iff_add_eq Nat.ModEq.add_left_cancel'
eq_pow_of_pell_lem 📖	—	Monoid.toNatPow Nat.instMonoid	—	—	LE.le.trans_lt Nat.cast_lt Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero LT.lt.le sub_le_sub_right covariant_swap_add_of_covariant_add sub_le_sub_left pow_le_pow_left₀ IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Nat.cast_zero Nat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_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.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.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.mul_congr
im_pellZd 📖	mathematical	—	Zsqrtd.im pellZd yn	—	—
isPell_iff_mem_unitary 📖	mathematical	—	IsPell 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	—	Unitary.mem_iff isPell_norm mul_comm
isPell_mul 📖	mathematical	IsPell	Zsqrtd Zsqrtd.instMul	—	isPell_norm StarMul.star_mul mul_comm mul_assoc mul_left_comm one_mul
isPell_nat 📖	mathematical	—	IsPell	—	Int.instCharZero Int.le_of_ofNat_le_ofNat le_of_lt
isPell_norm 📖	mathematical	—	IsPell Zsqrtd Zsqrtd.instMul Star.star Zsqrtd.instStar Zsqrtd.instOne	—	mul_comm mul_neg neg_add_cancel Nat.instAtLeastTwoHAddOfNat 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_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw 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.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 mul_one pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg add_zero Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr
isPell_one 📖	mathematical	—	IsPell	—	dz_val mul_one sub_sub_cancel
isPell_pellZd 📖	mathematical	—	IsPell pellZd	—	isPell_one pellZd_succ isPell_mul
isPell_star 📖	mathematical	—	IsPell Star.star Zsqrtd Zsqrtd.instStar	—	mul_neg neg_mul neg_neg
matiyasevic 📖	mathematical	—	xn yn Nat.ModEq	—	le_rfl yn_ge_n Dvd.dvd.trans ysq_dvd_yy y_dvd_iff dvd_mul_left Nat.modEq_zero_iff_dvd Nat.ModEq.trans yn_modEq_two Dvd.dvd.modEq_zero_nat dvd_mul_right xy_coprime dvd_of_mul_left_dvd mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono strictMono_y lt_trans zero_lt_one Nat.instZeroLEOneClass strictMono_x one_mul MulZeroClass.mul_zero add_zero lt_of_lt_of_le xy_modEq_of_modEq le_of_lt Nat.ModEq.dvd Nat.ModEq.symm Nat.ModEq.of_dvd yn_modEq_a_sub_one pell_eq eq_pell yn.congr_simp Nat.instCanonicallyOrderedAdd le_of_not_gt not_lt_of_ge mul_dvd_mul_left dvd_of_ysq_dvd lt_of_le_of_lt add_le_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Nat.instAtLeastTwoHAddOfNat two_mul modEq_of_xn_modEq not_le_of_gt Nat.ModEq.add_right
modEq_of_xn_modEq 📖	—	Nat.ModEq xn	—	—	mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono LT.lt.trans_le xn.congr_simp MulZeroClass.mul_zero add_zero add_assoc add_comm Nat.ModEq.trans xn_modEq_x4n_add Nat.ModEq.add_right Dvd.dvd.modEq_zero_nat dvd_rfl eq_of_xn_modEq' LT.lt.le Nat.ModEq.symm
n_lt_xn 📖	mathematical	—	xn	—	lt_of_lt_of_le xn_ge_a_pow
pellZd_add 📖	mathematical	—	pellZd Zsqrtd Zsqrtd.instMul	—	mul_one add_assoc pellZd_succ mul_assoc
pellZd_im 📖	mathematical	—	Zsqrtd.im pellZd yn	—	im_pellZd
pellZd_re 📖	mathematical	—	Zsqrtd.re pellZd xn	—	re_pellZd
pellZd_sub 📖	mathematical	—	pellZd Zsqrtd Zsqrtd.instMul Star.star Zsqrtd.instStar	—	pellZd_add add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub mul_comm mul_assoc isPell_norm isPell_pellZd mul_one
pellZd_succ 📖	mathematical	—	pellZd Zsqrtd Zsqrtd.instMul	—	Zsqrtd.ext Nat.cast_add Nat.cast_mul mul_one
pellZd_succ_succ 📖	mathematical	—	Zsqrtd Zsqrtd.instAdd pellZd Zsqrtd.instMul AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Zsqrtd.addGroupWithOne	—	Nat.instAtLeastTwoHAddOfNat Zsqrtd.natCast_val dz_val Zsqrtd.ext Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_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.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf 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.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add add_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one pellZd_succ mul_comm mul_left_comm add_comm Nat.cast_mul mul_add Distrib.leftDistribClass mul_one
pell_eq 📖	mathematical	—	xn yn	—	pell_eqz Nat.cast_le Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero add_eq_of_eq_sub'
pell_eqz 📖	mathematical	—	xz yz	—	isPell_pellZd
pell_val 📖	mathematical	—	pell xn yn	—	—
re_pellZd 📖	mathematical	—	Zsqrtd.re pellZd xn	—	—
strictMono_x 📖	mathematical	—	StrictMono Nat.instPreorder xn	—	lt_or_eq_of_le le_of_lt le_refl lt_of_lt_of_le lt_of_le_of_lt x_pos mul_one
strictMono_y 📖	mathematical	—	StrictMono Nat.instPreorder yn	—	lt_or_eq_of_le le_of_lt le_refl lt_of_le_of_lt mul_one mul_le_mul IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing IsOrderedRing.toMulPosMono x_pos
x_pos 📖	mathematical	—	xn	—	lt_of_le_of_lt n_lt_xn
x_sub_y_dvd_pow 📖	mathematical	—	yz Monoid.toNatPow Nat.instMonoid xz	—	Nat.cast_zero MulZeroClass.zero_mul pow_zero Nat.cast_one zero_add sub_self add_zero one_mul pow_one sub_add_cancel MulZeroClass.mul_zero Nat.instAtLeastTwoHAddOfNat pow_succ mul_comm Nat.cast_mul Nat.cast_pow mul_left_comm neg_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr 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.mul_pf_right 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_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsInt.to_isNat xz_succ_succ yz_succ_succ x_sub_y_dvd_pow_lem dvd_sub dvd_add Distrib.leftDistribClass Dvd.dvd.mul_left
x_sub_y_dvd_pow_lem 📖	—	—	—	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr 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.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_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat 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_add
xn_add 📖	mathematical	—	xn yn	—	pellZd_add Nat.cast_add Nat.cast_mul
xn_ge_a_pow 📖	mathematical	—	Monoid.toNatPow Nat.instMonoid xn	—	le_refl pow_succ le_trans
xn_modEq_x2n_add 📖	mathematical	—	Nat.ModEq xn	—	Nat.instAtLeastTwoHAddOfNat two_mul add_assoc xn_add zero_add Nat.ModEq.add Dvd.dvd.modEq_zero_nat dvd_mul_right yn_add left_distrib Distrib.leftDistribClass Dvd.dvd.mul_left xn_modEq_x2n_add_lem
xn_modEq_x2n_add_lem 📖	mathematical	—	xn yn	—	mul_assoc add_mul Distrib.rightDistribClass one_mul Nat.cast_add Nat.cast_mul Nat.cast_one add_eq_of_eq_sub' pell_eqz dvd_mul_right
xn_modEq_x2n_sub 📖	mathematical	—	Nat.ModEq xn	—	le_total xn_modEq_x2n_sub_lem tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub Nat.instAtLeastTwoHAddOfNat two_mul add_comm tsub_tsub_cancel_of_le IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
xn_modEq_x2n_sub_lem 📖	mathematical	—	Nat.ModEq xn	—	yz_sub mul_sub_left_distrib sub_add_eq_add_sub dvd_sub mul_comm xn_modEq_x2n_add_lem Dvd.dvd.mul_left dvd_mul_right Nat.instAtLeastTwoHAddOfNat two_mul add_tsub_assoc_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le xn_add add_assoc zero_add Nat.ModEq.add Dvd.dvd.modEq_zero_nat Nat.cast_add Nat.cast_mul
xn_modEq_x4n_add 📖	mathematical	—	Nat.ModEq xn	—	Nat.ModEq.add_right_cancel' Nat.ModEq.trans right_distrib Distrib.rightDistribClass add_assoc xn_modEq_x2n_add add_comm Nat.ModEq.symm
xn_modEq_x4n_sub 📖	mathematical	—	Nat.ModEq xn	—	le_trans le_refl Nat.ModEq.add_right_cancel' Nat.ModEq.trans right_distrib Distrib.rightDistribClass add_tsub_assoc_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le xn_modEq_x2n_add add_comm Nat.ModEq.symm xn_modEq_x2n_sub
xn_one 📖	mathematical	—	xn	—	one_mul MulZeroClass.mul_zero add_zero
xn_succ 📖	mathematical	—	xn yn	—	—
xn_succ_succ 📖	mathematical	—	xn	—	xy_succ_succ
xn_zero 📖	mathematical	—	xn	—	—
xy_coprime 📖	mathematical	—	xn yn	—	Nat.coprime_of_dvd' pell_eq Dvd.dvd.mul_left
xy_modEq_of_modEq 📖	mathematical	Nat.ModEq	xn yn	—	one_mul MulZeroClass.mul_zero add_zero MulZeroClass.zero_mul Nat.ModEq.add_right_cancel xn_succ_succ Nat.ModEq.mul Nat.ModEq.mul_left yn_succ_succ
xy_modEq_yn 📖	mathematical	—	Nat.ModEq Monoid.toNatPow Nat.instMonoid yn xn	—	xn.congr_simp MulZeroClass.mul_zero pow_zero yn.congr_simp zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub mul_one MulZeroClass.zero_mul Nat.ModEq.add Nat.ModEq.mul Nat.ModEq.refl Nat.modEq_zero_iff_dvd sq mul_dvd_mul dvd_mul_of_dvd_right Nat.ModEq.trans Nat.ModEq.of_dvd dvd_pow_self dvd_refl pow_succ Nat.ModEq.mul_right' add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero xn_add yn_add add_comm right_distrib Distrib.rightDistribClass
xy_succ_succ 📖	mathematical	—	xn yn	—	pellZd_succ_succ Zsqrtd.nsmul_val
xz_sub 📖	mathematical	—	xz yz	—	sub_eq_add_neg mul_neg pellZd_sub
xz_succ 📖	mathematical	—	xz az yz	—	—
xz_succ_succ 📖	mathematical	—	xz	—	eq_sub_of_add_eq xn_succ_succ
y_dvd_iff 📖	mathematical	—	yn	—	y_mul_dvd xy_coprime ne_of_lt strictMono_y eq_zero_of_zero_dvd not_le_of_gt Dvd.dvd.mul_left yn_add
y_mul_dvd 📖	mathematical	—	yn	—	dvd_zero yn_add dvd_add Distrib.leftDistribClass dvd_mul_left Dvd.dvd.mul_right
yn_add 📖	mathematical	—	yn xn	—	pellZd_add Nat.cast_add Nat.cast_mul
yn_ge_n 📖	mathematical	—	yn	—	lt_of_le_of_lt strictMono_y
yn_modEq_a_sub_one 📖	mathematical	—	Nat.ModEq yn	—	MulZeroClass.zero_mul add_zero Nat.ModEq.add_right_cancel yn_succ_succ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Nat.ModEq.mul Nat.ModEq.mul_left Nat.modEq_sub LT.lt.le
yn_modEq_two 📖	mathematical	—	Nat.ModEq yn	—	MulZeroClass.zero_mul add_zero Nat.ModEq.add_right_cancel yn_succ_succ mul_assoc Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Nat.ModEq.trans Dvd.dvd.modEq_zero_nat dvd_mul_right Dvd.dvd.zero_modEq_nat
yn_one 📖	mathematical	—	yn	—	MulZeroClass.zero_mul add_zero
yn_succ 📖	mathematical	—	yn xn	—	—
yn_succ_succ 📖	mathematical	—	yn	—	xy_succ_succ
yn_zero 📖	mathematical	—	yn	—	—
ysq_dvd_yy 📖	mathematical	—	yn	—	Nat.modEq_zero_iff_dvd Nat.ModEq.trans Nat.ModEq.of_dvd pow_succ pow_zero one_mul xy_modEq_yn mul_assoc
yz_sub 📖	mathematical	—	yz xz	—	sub_eq_add_neg mul_neg mul_comm add_comm pellZd_sub
yz_succ 📖	mathematical	—	yz xz az	—	—
yz_succ_succ 📖	mathematical	—	yz	—	eq_sub_of_add_eq yn_succ_succ

---

← Back to Index