Dioph

📁 Source: Mathlib/NumberTheory/Dioph.lean

Statistics

Metric	Count
Definitions `Dioph`, `DiophFn`, `DiophPFun`, `«term&_»`, `«termD&_»`, `_»`, `«termD∃»`, `«termD≡»`, `«term_D%_»`, `«term_D*_»`, `«term_D+_»`, `«term_D-_»`, `«term_D/_»`, `«term_D<_»`, `«term_D=_»`, `«term_D∣_»`, `«term_D∧_»`, `«term_D∨_»`, `«term_D≠_»`, `«term_D≤_»`, `Poly`, `const`, `instAdd`, `instAddCommGroup`, `instAddGroupWithOne`, `instCommRing`, `instFunLike`, `instInhabited`, `instMul`, `instNeg`, `instOne`, `instSub`, `instZero`, `map`, `proj`, `sumsq`	36
Theorems `forall`, `abs_poly_dioph`, `add_dioph`, `const_dioph`, `diophFn_comp`, `diophFn_comp1`, `diophFn_comp2`, `diophFn_compn`, `diophFn_iff_pFun`, `diophFn_vec`, `diophFn_vec_comp1`, `diophPFun_comp1`, `diophPFun_vec`, `dioph_comp`, `dioph_comp2`, `div_dioph`, `dom_dioph`, `dvd_dioph`, `eq_dioph`, `ex1_dioph`, `ex_dioph`, `ext`, `inject_dummies`, `inject_dummies_lem`, `inter`, `le_dioph`, `lt_dioph`, `modEq_dioph`, `mod_dioph`, `mul_dioph`, `ne_dioph`, `of_no_dummies`, `pell_dioph`, `pow_dioph`, `proj_dioph`, `proj_dioph_of_nat`, `reindex_dioph`, `reindex_diophFn`, `sub_dioph`, `union`, `vec_ex1_dioph`, `xn_dioph`, `add`, `neg`, `add_apply`, `coe_add`, `coe_mul`, `coe_neg`, `coe_one`, `coe_sub`, `coe_zero`, `const_apply`, `ext`, `ext_iff`, `induction`, `isPoly`, `map_apply`, `mul_apply`, `neg_apply`, `one_apply`, `proj_apply`, `sub_apply`, `sumsq_eq_zero`, `sumsq_nonneg`, `zero_apply`	65
Total	101

Dioph

Definitions

Name	Category	Theorems
`DiophFn` 📖	MathDef	6 math math: `diophFn_vec`, `const_dioph`, `proj_dioph`, `diophFn_iff_pFun`, `proj_dioph_of_nat`, `abs_poly_dioph`
`DiophPFun` 📖	MathDef	3 math math: `xn_dioph`, `diophPFun_vec`, `diophFn_iff_pFun`
`«term&_»` 📖	CompOp	—
`«termD&_»` 📖	CompOp	—
`«termD._»` 📖	CompOp	—
`«termD∃»` 📖	CompOp	—
`«termD≡»` 📖	CompOp	—
`«term_D%_»` 📖	CompOp	—
`«term_D*_»` 📖	CompOp	—
`«term_D+_»` 📖	CompOp	—
`«term_D-_»` 📖	CompOp	—
`«term_D/_»` 📖	CompOp	—
`«term_D<_»` 📖	CompOp	—
`«term_D=_»` 📖	CompOp	—
`«term_D∣_»` 📖	CompOp	—
`«term_D∧_»` 📖	CompOp	—
`«term_D∨_»` 📖	CompOp	—
`«term_D≠_»` 📖	CompOp	—
`«term_D≤_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_poly_dioph` 📖	mathematical	—	`DiophFn` `DFunLike.coe` `Poly` `Poly.instFunLike`	—	`of_no_dummies`
`add_dioph` 📖	—	`DiophFn`	—	—	`diophFn_comp2` `abs_poly_dioph` `Fin2.IsLT.zero` `Fin2.IsLT.succ`
`const_dioph` 📖	mathematical	—	`DiophFn`	—	`abs_poly_dioph`
`diophFn_comp` 📖	—	`DiophFn` `Fin2` `VectorAllP`	—	—	`dioph_comp` `diophFn_vec` `proj_dioph` `vectorAllP_iff_forall` `reindex_diophFn`
`diophFn_comp1` 📖	mathematical	`Dioph` `DiophFn`	`setOf` `Set` `Set.instMembership` `Option.elim'`	—	`ext` `diophPFun_comp1` `diophFn_iff_pFun`
`diophFn_comp2` 📖	—	`DiophFn` `Fin2` `Fin2.ofNat'` `Fin2.IsLT.zero` `Fin2.IsLT.succ`	—	—	`Fin2.IsLT.zero` `Fin2.IsLT.succ` `diophFn_comp`
`diophFn_compn` 📖	mathematical	`Dioph` `Fin2` `VectorAllP` `DiophFn`	`setOf` `Set` `Set.instMembership`	—	`ext` `reindex_dioph` `diophFn_comp1` `reindex_diophFn`
`diophFn_iff_pFun` 📖	mathematical	—	`DiophFn` `DiophPFun` `PFun.lift`	—	`Set.ext` `PFun.lift_graph`
`diophFn_vec` 📖	mathematical	—	`DiophFn` `Fin2` `Dioph` `setOf` `Fin2.fs` `Fin2.fz`	—	`reindex_dioph`
`diophFn_vec_comp1` 📖	mathematical	`Dioph` `Fin2` `DiophFn`	`setOf` `Vector3` `Set` `Set.instMembership` `Vector3.cons`	—	`ext` `diophFn_comp1` `reindex_dioph`
`diophPFun_comp1` 📖	mathematical	`Dioph` `DiophPFun`	`setOf` `PFun.Dom` `Set` `Set.instMembership` `Option.elim'` `PFun.fn`	—	`ext` `ex1_dioph` `inter` `PFun.fn.eq_1`
`diophPFun_vec` 📖	mathematical	—	`DiophPFun` `Fin2` `Dioph` `setOf` `PFun.graph` `Vector3` `Fin2.fs` `Fin2.fz`	—	`reindex_dioph`
`dioph_comp` 📖	mathematical	`Dioph` `Fin2` `VectorAllP` `DiophFn`	`setOf` `Set` `Vector3` `Set.instMembership`	—	`diophFn_compn` `reindex_dioph`
`dioph_comp2` 📖	—	`DiophFn` `Dioph` `Fin2` `Fin2.ofNat'` `Fin2.IsLT.zero` `Fin2.IsLT.succ`	—	—	`Fin2.IsLT.zero` `Fin2.IsLT.succ` `dioph_comp`
`div_dioph` 📖	—	`DiophFn`	—	—	`Fin2.IsLT.succ` `Fin2.IsLT.zero` `union` `inter` `eq_dioph` `proj_dioph_of_nat` `const_dioph` `le_dioph` `mul_dioph` `lt_dioph` `add_dioph` `diophFn_comp2` `diophFn_vec` `ext` `vectorAll_iff_forall` `le_antisymm_iff`
`dom_dioph` 📖	mathematical	`DiophPFun`	`Dioph` `PFun.Dom`	—	`Set.ext` `PFun.dom_iff_graph` `ex1_dioph`
`dvd_dioph` 📖	mathematical	`DiophFn`	`Dioph`	—	`dioph_comp` `Fin2.IsLT.succ` `Fin2.IsLT.zero` `vec_ex1_dioph` `eq_dioph` `proj_dioph_of_nat` `mul_dioph`
`eq_dioph` 📖	mathematical	`DiophFn`	`Dioph`	—	`dioph_comp2` `of_no_dummies` `Fin2.IsLT.zero` `Fin2.IsLT.succ` `sub_eq_zero_of_eq` `eq_of_sub_eq_zero`
`ex1_dioph` 📖	mathematical	`Dioph`	`setOf` `Set` `Set.instMembership` `Option.elim'`	—	—
`ex_dioph` 📖	mathematical	`Dioph`	`setOf` `Set` `Set.instMembership`	—	—
`ext` 📖	—	`Dioph` `Set` `Set.instMembership`	—	—	`Set.ext`
`inject_dummies` 📖	—	`DFunLike.coe` `Poly` `Poly.instFunLike`	—	—	`inject_dummies_lem`
`inject_dummies_lem` 📖	mathematical	—	`DFunLike.coe` `Poly` `Poly.instFunLike` `Poly.map`	—	—
`inter` 📖	mathematical	`Dioph`	`Set` `Set.instInter`	—	`DiophList.forall`
`le_dioph` 📖	mathematical	`DiophFn`	`Dioph` `setOf`	—	`dioph_comp2` `ext` `Fin2.IsLT.succ` `Fin2.IsLT.zero` `vec_ex1_dioph` `eq_dioph` `add_dioph` `proj_dioph_of_nat`
`lt_dioph` 📖	mathematical	`DiophFn`	`Dioph` `setOf`	—	`le_dioph` `add_dioph` `const_dioph`
`modEq_dioph` 📖	mathematical	`DiophFn`	`Dioph` `Nat.ModEq`	—	`eq_dioph` `mod_dioph`
`mod_dioph` 📖	—	`DiophFn`	—	—	`Fin2.IsLT.succ` `Fin2.IsLT.zero` `inter` `union` `eq_dioph` `proj_dioph_of_nat` `const_dioph` `lt_dioph` `vec_ex1_dioph` `add_dioph` `mul_dioph` `diophFn_comp2` `diophFn_vec` `ext` `vectorAll_iff_forall`
`mul_dioph` 📖	—	`DiophFn`	—	—	`diophFn_comp2` `abs_poly_dioph` `Fin2.IsLT.zero` `Fin2.IsLT.succ`
`ne_dioph` 📖	mathematical	`DiophFn`	`Dioph` `setOf`	—	`ext` `union` `lt_dioph` `lt_or_lt_iff_ne`
`of_no_dummies` 📖	mathematical	`DFunLike.coe` `Poly` `Poly.instFunLike`	`Dioph`	—	—
`pell_dioph` 📖	mathematical	—	`Dioph` `Fin2` `Fin2.ofNat'` `Fin2.IsLT.zero` `Pell.xn` `Fin2.IsLT.succ` `Pell.yn`	—	`Fin2.IsLT.zero` `Fin2.IsLT.succ` `inter` `lt_dioph` `const_dioph` `proj_dioph_of_nat` `le_dioph` `union` `eq_dioph` `vec_ex1_dioph` `sub_dioph` `mul_dioph` `modEq_dioph` `dvd_dioph` `ext` `Pell.matiyasevic`
`pow_dioph` 📖	mathematical	`DiophFn`	`Monoid.toNatPow` `Nat.instMonoid`	—	`Fin2.IsLT.succ` `Fin2.IsLT.zero` `union` `inter` `eq_dioph` `proj_dioph_of_nat` `const_dioph` `lt_dioph` `vec_ex1_dioph` `reindex_dioph` `pell_dioph` `modEq_dioph` `add_dioph` `mul_dioph` `sub_dioph` `le_dioph` `diophFn_comp2` `diophFn_vec` `ext` `Pell.eq_pow_of_pell`
`proj_dioph` 📖	mathematical	—	`DiophFn`	—	`abs_poly_dioph`
`proj_dioph_of_nat` 📖	mathematical	—	`DiophFn` `Fin2` `Fin2.ofNat'`	—	`proj_dioph`
`reindex_dioph` 📖	mathematical	`Dioph`	`setOf` `Set` `Set.instMembership`	—	—
`reindex_diophFn` 📖	—	`DiophFn`	—	—	`reindex_dioph`
`sub_dioph` 📖	—	`DiophFn`	—	—	`diophFn_comp2` `Fin2.IsLT.zero` `Fin2.IsLT.succ` `diophFn_vec` `ext` `union` `eq_dioph` `proj_dioph_of_nat` `add_dioph` `inter` `le_dioph` `const_dioph` `vectorAll_iff_forall` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `tsub_eq_zero_iff_le` `Nat.instCanonicallyOrderedAdd`
`union` 📖	mathematical	`Dioph`	`Set` `Set.instUnion`	—	`inject_dummies_lem` `mul_eq_zero` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE`
`vec_ex1_dioph` 📖	mathematical	`Dioph` `Fin2`	`setOf` `Vector3` `Set` `Set.instMembership` `Vector3.cons`	—	`ext` `ex1_dioph` `reindex_dioph`
`xn_dioph` 📖	mathematical	—	`DiophPFun` `Fin2` `Fin2.ofNat'` `Fin2.IsLT.zero` `Pell.xn` `Fin2.IsLT.succ`	—	`Fin2.IsLT.succ` `Fin2.IsLT.zero` `reindex_dioph` `pell_dioph` `vec_ex1_dioph` `diophPFun_vec` `ext`

Dioph.DiophList

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forall` 📖	mathematical	`List.Forall` `Set` `Dioph`	`setOf` `Set.instMembership`	—	`List.forall_cons` `List.Forall.imp` `Poly.sumsq_eq_zero`

IsPoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsPoly`	`Pi.instAdd`	—	`sub_neg_eq_add` `neg`
`neg` 📖	mathematical	`IsPoly`	`Pi.instNeg`	—	`zero_sub`

Poly

Definitions

Name	Category	Theorems
`const` 📖	CompOp	3 math math: `const_apply`, `coe_zero`, `coe_one`
`instAdd` 📖	CompOp	2 math math: `coe_add`, `add_apply`
`instAddCommGroup` 📖	CompOp	—
`instAddGroupWithOne` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instFunLike` 📖	CompOp	21 math math: `const_apply`, `coe_zero`, `neg_apply`, `Dioph.inject_dummies_lem`, `proj_apply`, `sumsq_nonneg`, `ext_iff`, `isPoly`, `coe_mul`, `coe_sub`, `coe_add`, `one_apply`, `sumsq_eq_zero`, `add_apply`, `coe_one`, `zero_apply`, `map_apply`, `coe_neg`, `Dioph.abs_poly_dioph`, `mul_apply`, `sub_apply`
`instInhabited` 📖	CompOp	—
`instMul` 📖	CompOp	2 math math: `coe_mul`, `mul_apply`
`instNeg` 📖	CompOp	2 math math: `neg_apply`, `coe_neg`
`instOne` 📖	CompOp	2 math math: `one_apply`, `coe_one`
`instSub` 📖	CompOp	2 math math: `coe_sub`, `sub_apply`
`instZero` 📖	CompOp	2 math math: `coe_zero`, `zero_apply`
`map` 📖	CompOp	2 math math: `Dioph.inject_dummies_lem`, `map_apply`
`proj` 📖	CompOp	1 math math: `proj_apply`
`sumsq` 📖	CompOp	2 math math: `sumsq_nonneg`, `sumsq_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instAdd`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instAdd` `Pi.instAdd`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instMul` `Pi.instMul`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instNeg` `Pi.instNeg`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instOne` `const`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instSub` `Pi.instSub`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instZero` `const`	—	—
`const_apply` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `const`	—	—
`ext` 📖	—	`DFunLike.coe` `Poly` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike`	—	`ext`
`induction` 📖	—	`proj` `const` `Poly` `instSub` `instMul`	—	—	—
`isPoly` 📖	mathematical	—	`IsPoly` `DFunLike.coe` `Poly` `instFunLike`	—	—
`map_apply` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `map`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instMul`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instNeg`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instOne`	—	—
`proj_apply` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `proj`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instSub`	—	—
`sumsq_eq_zero` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `sumsq` `List.Forall`	—	`Int.instAddLeftMono` `covariant_swap_add_of_covariant_add` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `IsStrictOrderedRing.noZeroDivisors`
`sumsq_nonneg` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `sumsq`	—	`le_refl` `sumsq.eq_2` `add_nonneg` `Int.instAddLeftMono` `mul_self_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing`
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `Poly` `instFunLike` `instZero`	—	—

(root)

Definitions

Name	Category	Theorems
`Dioph` 📖	MathDef	11 math math: `Dioph.diophFn_vec`, `Dioph.le_dioph`, `Dioph.lt_dioph`, `Dioph.of_no_dummies`, `Dioph.modEq_dioph`, `Dioph.ne_dioph`, `Dioph.dom_dioph`, `Dioph.eq_dioph`, `Dioph.diophPFun_vec`, `Dioph.pell_dioph`, `Dioph.dvd_dioph`
`Poly` 📖	CompOp	21 math math: `Poly.const_apply`, `Poly.coe_zero`, `Poly.neg_apply`, `Dioph.inject_dummies_lem`, `Poly.proj_apply`, `Poly.sumsq_nonneg`, `Poly.ext_iff`, `Poly.isPoly`, `Poly.coe_mul`, `Poly.coe_sub`, `Poly.coe_add`, `Poly.one_apply`, `Poly.sumsq_eq_zero`, `Poly.add_apply`, `Poly.coe_one`, `Poly.zero_apply`, `Poly.map_apply`, `Poly.coe_neg`, `Dioph.abs_poly_dioph`, `Poly.mul_apply`, `Poly.sub_apply`

---

← Back to Index