Documentation Verification Report

Roth

📁 Source: Mathlib/Combinatorics/Additive/Corner/Roth.lean

Statistics

Metric	Count
Definitions `cornersTheoremBound`	1
Theorems `corners_theorem`, `corners_theorem_nat`, `rothNumberNat_isLittleO_id`, `roth_3ap_theorem`, `roth_3ap_theorem_nat`	5
Total	6

(root)

Definitions

Name	Category	Theorems
`cornersTheoremBound` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`corners_theorem` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `cornersTheoremBound` `Fintype.card` `Real.instLE` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instNatCast` `Finset.card`	`IsCornerFree` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`LE.le.trans` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Finset.card_le_univ` `mul_le_iff_le_one_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_pos'` `NeZero.charZero_one` `Fintype.card_pos` `AddTorsor.nonempty` `sq` `Fintype.card_prod` `Nat.cast_mul` `LT.lt.not_ge` `inv_lt_iff_one_lt_mul₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `SimpleGraph.triangleRemovalBound_pos` `div_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.floor_lt'` `ne_of_gt` `cornersTheoremBound.eq_1` `le_of_mul_le_mul_right` `Nat.instAtLeastTwoHAddOfNat` `SimpleGraph.FarFromTriangleFree.le_card_cliqueFinset` `Fintype.card_sum` `Nat.cast_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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_one` `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.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_congr` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `one_mul` `SimpleGraph.TripartiteFromTriangles.card_triangles` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass`
`corners_theorem_nat` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `cornersTheoremBound` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Finset` `Finset.instHasSubset` `SProd.sprod` `Finset.instSProd` `Finset.range` `Real.instLE` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Finset.card`	`IsCornerFree` `Nat.instAddCommMonoid` `SetLike.coe` `Finset.instSetLike`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.image_image` `Set.image_congr` `Finset.coe_product` `Finset.coe_subset` `Finset.coe_range` `Set.image_id` `Fin.isAddFreimanIso_Iio` `two_ne_zero` `le_refl` `IsCornerFree.of_image` `IsAddFreimanIso.isAddFreimanHom` `Function.Injective.injOn` `Fin.val_injective` `Set.image_subset_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Fin.natCast_strictMono` `corners_theorem` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Fintype.card_fin` `Nat.cast_add` `Nat.cast_mul` `Nat.cast_one` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `pow_le_pow_left₀` `IsOrderedRing.toMulPosMono` `le_of_lt` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_nonneg` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `add_le_add_right` `RCLike.charZero_rclike` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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.pow_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `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.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.one_pow` `Finset.card_image_of_injOn` `Set.InjOn.mono` `CharP.natCast_injOn_Iio` `Fin.charP` `AddRightCancelSemigroup.toIsRightCancelAdd` `Set.InjOn.prodMap` `Finset.coe_image`
`rothNumberNat_isLittleO_id` 📖	mathematical	—	`Asymptotics.IsLittleO` `Real` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Real.instNatCast` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `rothNumberNat`	—	`RCLike.norm_natCast` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Nat.instAtLeastTwoHAddOfNat` `rothNumberNat_spec` `not_lt` `roth_3ap_theorem_nat` `LT.lt.le`
`roth_3ap_theorem` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `cornersTheoremBound` `Fintype.card` `Real.instLE` `Real.instMul` `Real.instNatCast` `Finset.card`	`ThreeAPFree` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`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.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Fintype.card_pos` `AddTorsor.nonempty` `Finset.card_univ` `Finset.card_product` `Finset.card_equiv` `add_sub_cancel_left` `Finset.coe_filter` `corners_theorem` `sub_add_sub_comm` `add_comm` `add_sub_add_comm` `add_right_cancel_iff` `AddRightCancelSemigroup.toIsRightCancelAdd` `sub_eq_sub_iff_add_eq_add`
`roth_3ap_theorem_nat` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `cornersTheoremBound` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Finset` `Finset.instHasSubset` `Finset.range` `Real.instLE` `Real.instMul` `Finset.card`	`ThreeAPFree` `Nat.instAddMonoid` `SetLike.coe` `Finset.instSetLike`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.image_image` `Set.image_congr` `Finset.coe_range` `Finset.coe_subset` `Set.image_id` `Fin.isAddFreimanIso_Iio` `two_ne_zero` `le_refl` `ThreeAPFree.of_image` `IsAddFreimanIso.isAddFreimanHom` `Function.Injective.injOn` `Fin.val_injective` `Set.image_subset_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Fin.natCast_strictMono` `roth_3ap_theorem` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Fintype.card_fin` `Nat.cast_add` `Nat.cast_mul` `Nat.cast_one` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `le_of_lt` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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_congr` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `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.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Finset.card_image_of_injOn` `Set.InjOn.mono` `CharP.natCast_injOn_Iio` `Fin.charP` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.coe_image`

---

← Back to Index