Xgcd

📁 Source: Mathlib/Data/PNat/Xgcd.lean

Statistics

Metric	Count
Definitions XgcdType, IsReduced, IsReduced', IsSpecial, IsSpecial', a, ap, b, bp, finish, flip, instRepr, instSizeOf, mk', q, qp, r, reduce, start, step, succ₂, v, vp, w, wp, x, y, z, zp, gcdA', gcdB', gcdD, gcdW, gcdX, gcdY, gcdZ, instInhabitedXgcdType, default, xgcd	39
Theorems finish_isReduced, finish_isSpecial, finish_v, flip_a, flip_b, flip_isReduced, flip_isSpecial, flip_v, flip_w, flip_x, flip_y, flip_z, isReduced_iff, isSpecial_iff, qp_eq, reduce_a, reduce_b, reduce_isReduced, reduce_isReduced', reduce_isSpecial, reduce_isSpecial', reduce_v, rq_eq, start_isSpecial, start_v, step_isSpecial, step_v, step_wf, v_eq_succ_vp, gcdA'_coe, gcdB'_coe, gcd_a_eq, gcd_b_eq, gcd_det_eq, gcd_eq, gcd_props, gcd_rel_left, gcd_rel_left', gcd_rel_right, gcd_rel_right'	40
Total	79

PNat

Definitions

Name	Category	Theorems
XgcdType 📖	CompData	1 math math: XgcdType.step_wf
gcdA' 📖	CompOp	5 math math: gcd_props, gcd_rel_left', gcd_rel_right', gcdA'_coe, gcd_a_eq
gcdB' 📖	CompOp	5 math math: gcd_b_eq, gcd_props, gcdB'_coe, gcd_rel_left', gcd_rel_right'
gcdD 📖	CompOp	2 math math: gcd_props, gcd_eq
gcdW 📖	CompOp	5 math math: gcd_props, gcd_rel_right, gcd_det_eq, gcd_rel_right', gcdA'_coe
gcdX 📖	CompOp	5 math math: gcd_rel_left, gcd_props, gcd_det_eq, gcd_rel_left', gcdA'_coe
gcdY 📖	CompOp	5 math math: gcd_props, gcd_rel_right, gcd_det_eq, gcdB'_coe, gcd_rel_right'
gcdZ 📖	CompOp	5 math math: gcd_rel_left, gcd_props, gcd_det_eq, gcdB'_coe, gcd_rel_left'
instInhabitedXgcdType 📖	CompOp	—
xgcd 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gcdA'_coe 📖	mathematical	—	val gcdA' gcdW gcdX	—	add_right_comm
gcdB'_coe 📖	mathematical	—	val gcdB' gcdY gcdZ	—	add_assoc
gcd_a_eq 📖	mathematical	—	PNat instMulPNat gcdA' gcd	—	gcd_props gcd_eq
gcd_b_eq 📖	mathematical	—	PNat instMulPNat gcdB' gcd	—	gcd_props gcd_eq
gcd_det_eq 📖	mathematical	—	PNat instMulPNat gcdW gcdZ Nat.succPNat gcdX gcdY	—	gcd_props
gcd_eq 📖	mathematical	—	gcdD gcd	—	gcd_props dvd_antisymm dvd_gcd Dvd.intro mul_comm Dvd.dvd.trans dvd_mul_left dvd_iff
gcd_props 📖	mathematical	—	PNat instMulPNat gcdW gcdZ Nat.succPNat gcdX gcdY gcdA' gcdD gcdB' val	—	XgcdType.reduce_isReduced' gcdA'_coe gcdB'_coe XgcdType.reduce_isSpecial' mul_coe Nat.succPNat_coe XgcdType.reduce_v XgcdType.start_v add_mul Distrib.rightDistribClass eq mul_add Distrib.leftDistribClass mul_comm 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
gcd_rel_left 📖	mathematical	—	val gcdZ gcdX gcd	—	gcd_props gcd_eq
gcd_rel_left' 📖	mathematical	—	PNat instMulPNat gcdZ gcdA' Nat.succPNat gcdX val gcdB'	—	gcd_props
gcd_rel_right 📖	mathematical	—	val gcdW gcdY gcd	—	gcd_props gcd_eq
gcd_rel_right' 📖	mathematical	—	PNat instMulPNat gcdW gcdB' Nat.succPNat gcdY val gcdA'	—	gcd_props

PNat.XgcdType

Definitions

Name	Category	Theorems
IsReduced 📖	MathDef	4 math math: flip_isReduced, reduce_isReduced, isReduced_iff, finish_isReduced
IsReduced' 📖	MathDef	2 math math: reduce_isReduced', isReduced_iff
IsSpecial 📖	MathDef	3 math math: flip_isSpecial, start_isSpecial, isSpecial_iff
IsSpecial' 📖	MathDef	2 math math: isSpecial_iff, reduce_isSpecial'
a 📖	CompOp	2 math math: flip_b, flip_a
ap 📖	CompOp	1 math math: rq_eq
b 📖	CompOp	2 math math: flip_b, flip_a
bp 📖	CompOp	1 math math: rq_eq
finish 📖	CompOp	4 math math: finish_v, reduce_a, finish_isSpecial, finish_isReduced
flip 📖	CompOp	10 math math: flip_y, flip_b, flip_isSpecial, flip_isReduced, flip_x, reduce_b, flip_w, flip_a, flip_v, flip_z
instRepr 📖	CompOp	—
instSizeOf 📖	CompOp	1 math math: step_wf
mk' 📖	CompOp	—
q 📖	CompOp	2 math math: rq_eq, qp_eq
qp 📖	CompOp	1 math math: qp_eq
r 📖	CompOp	1 math math: rq_eq
reduce 📖	CompOp	7 math math: reduce_isReduced', reduce_a, reduce_v, reduce_isSpecial, reduce_b, reduce_isReduced, reduce_isSpecial'
start 📖	CompOp	2 math math: start_isSpecial, start_v
step 📖	CompOp	4 math math: step_isSpecial, step_wf, reduce_b, step_v
succ₂ 📖	CompOp	1 math math: v_eq_succ_vp
v 📖	CompOp	6 math math: finish_v, reduce_v, v_eq_succ_vp, flip_v, step_v, start_v
vp 📖	CompOp	1 math math: v_eq_succ_vp
w 📖	CompOp	2 math math: flip_w, flip_z
wp 📖	CompOp	—
x 📖	CompOp	2 math math: flip_y, flip_x
y 📖	CompOp	2 math math: flip_y, flip_x
z 📖	CompOp	2 math math: flip_w, flip_z
zp 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finish_isReduced 📖	mathematical	—	IsReduced finish	—	—
finish_isSpecial 📖	mathematical	IsSpecial	finish	—	add_mul Distrib.rightDistribClass add_comm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr 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.add_pf_add_gt Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat
finish_v 📖	mathematical	r	v finish	—	rq_eq zero_add qp_eq 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt
flip_a 📖	mathematical	—	a flip b	—	—
flip_b 📖	mathematical	—	b flip a	—	—
flip_isReduced 📖	mathematical	—	IsReduced flip	—	—
flip_isSpecial 📖	mathematical	—	IsSpecial flip	—	mul_comm add_comm
flip_v 📖	mathematical	—	v flip	—	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.add_pf_add_gt
flip_w 📖	mathematical	—	w flip z	—	—
flip_x 📖	mathematical	—	x flip y	—	—
flip_y 📖	mathematical	—	y flip x	—	—
flip_z 📖	mathematical	—	z flip w	—	—
isReduced_iff 📖	mathematical	—	IsReduced IsReduced'	—	—
isSpecial_iff 📖	mathematical	—	IsSpecial IsSpecial'	—	Mathlib.Tactic.Ring.of_eq 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul one_mul mul_one
qp_eq 📖	mathematical	r	q qp	—	rq_eq add_zero MulZeroClass.mul_zero
reduce_a 📖	mathematical	r	reduce finish	—	reduce.eq_1
reduce_b 📖	mathematical	—	reduce flip step	—	reduce.eq_1
reduce_isReduced 📖	mathematical	—	IsReduced reduce	—	reduce_a finish_isReduced step_wf reduce_b flip_isReduced
reduce_isReduced' 📖	mathematical	—	IsReduced' reduce	—	isReduced_iff reduce_isReduced
reduce_isSpecial 📖	mathematical	IsSpecial	reduce	—	reduce_a finish_isSpecial step_wf reduce_b flip_isSpecial step_isSpecial
reduce_isSpecial' 📖	mathematical	IsSpecial	IsSpecial' reduce	—	isSpecial_iff reduce_isSpecial
reduce_v 📖	mathematical	—	v reduce	—	reduce_a finish_v step_wf reduce_b flip_v step_v
rq_eq 📖	mathematical	—	r bp q ap	—	—
start_isSpecial 📖	mathematical	—	IsSpecial start	—	—
start_v 📖	mathematical	—	v start PNat.val	—	PNat.pos
step_isSpecial 📖	mathematical	IsSpecial	step	—	mul_add Distrib.leftDistribClass mul_comm 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.add_pf_add_gt Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat
step_v 📖	mathematical	—	v step	—	rq_eq add_comm add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub 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.add_pf_add_gt
step_wf 📖	mathematical	—	PNat.XgcdType instSizeOf step	—	—
v_eq_succ_vp 📖	mathematical	—	v succ₂ vp	—	Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.RingNF.add_assoc_rev

PNat.instInhabitedXgcdType

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index