Defs

📁 Source: Mathlib/Combinatorics/Additive/AP/Three/Defs.lean

Statistics

Metric	Count
Definitions `ThreeAPFree`, `instDecidable`, `ThreeGPFree`, `instDecidable`, `addRothNumber`, `mulRothNumber`, `rothNumberNat`	7
Theorems `addRothNumber_eq_rothNumberNat`, `addRothNumber_le_rothNumberNat`, `addRothNumber_mono`, `threeAPFree`, `addRothNumber_congr`, `threeAPFree_congr`, `mulRothNumber_mono`, `threeGPFree`, `mulRothNumber_congr`, `threeGPFree_congr`, `threeAPFree`, `threeGPFree`, `addRothNumber_eq`, `eq_right`, `image`, `image'`, `le_addRothNumber`, `le_rothNumberNat`, `mono`, `of_image`, `prod`, `vadd_set`, `eq_right`, `image`, `image'`, `le_mulRothNumber`, `mono`, `mulRothNumber_eq`, `of_image`, `prod`, `smul_set`, `smul_set₀`, `addRothNumber_Ico`, `addRothNumber_empty`, `addRothNumber_le`, `addRothNumber_lt_of_forall_not_threeAPFree`, `addRothNumber_map_add_left`, `addRothNumber_map_add_right`, `addRothNumber_singleton`, `addRothNumber_spec`, `addRothNumber_union_le`, `le_addRothNumber_product`, `le_mulRothNumber_product`, `mulRothNumber_empty`, `mulRothNumber_le`, `mulRothNumber_lt_of_forall_not_threeGPFree`, `mulRothNumber_map_mul_left`, `mulRothNumber_map_mul_right`, `mulRothNumber_singleton`, `mulRothNumber_spec`, `mulRothNumber_union_le`, `rothNumberNat_add_le`, `rothNumberNat_def`, `rothNumberNat_le`, `rothNumberNat_spec`, `rothNumberNat_zero`, `threeAPFree_empty`, `threeAPFree_iff_eq_right`, `threeAPFree_image`, `threeAPFree_insert`, `threeAPFree_insert_of_lt`, `threeAPFree_pi`, `threeAPFree_singleton`, `threeAPFree_vadd_set`, `threeGPFree_empty`, `threeGPFree_image`, `threeGPFree_insert`, `threeGPFree_insert_of_lt`, `threeGPFree_pi`, `threeGPFree_singleton`, `threeGPFree_smul_set`, `threeGPFree_smul_set₀`	72
Total	79

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addRothNumber_eq_rothNumberNat` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `AddMonoidWithOne.toAddMonoid` `instAddMonoidWithOne` `Finset.Iio` `instPartialOrder` `instLocallyFiniteOrderBot` `rothNumberNat`	—	`IsAddFreimanIso.addRothNumber_congr` `Finset.coe_Iio` `Finset.coe_range` `isAddFreimanIso_Iio` `two_ne_zero`
`addRothNumber_le_rothNumberNat` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `Finset.Iio` `instPartialOrder` `instLocallyFiniteOrderBot` `AddMonoidWithOne.toNatCast` `rothNumberNat`	—	`Finset.coe_range` `Finset.coe_Iio` `natCast_strictMono` `Set.InjOn.mono` `CharP.natCast_injOn_Iio` `charP` `AddRightCancelSemigroup.toIsRightCancelAdd` `val_cast_of_lt` `cast_val_eq_self` `IsAddFreimanHom.addRothNumber_mono` `AddMonoidHomClass.isAddFreimanHom` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Set.BijOn.mapsTo`

IsAddFreimanHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addRothNumber_mono` 📖	mathematical	`IsAddFreimanHom` `SetLike.coe` `Finset` `Finset.instSetLike` `Set.BijOn`	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `AddCommMonoid.toAddMonoid`	—	`addRothNumber_spec` `Zero.instNonempty` `Set.MapsTo.image_subset` `Set.MapsTo.mono` `Set.SurjOn.mapsTo_invFunOn` `Set.BijOn.surjOn` `Finset.coe_subset` `Finset.Subset.rfl` `Set.SurjOn.mono` `Finset.card_image_of_injOn` `Set.InjOn.mono` `Function.invFunOn_injOn_image` `ThreeAPFree.le_addRothNumber` `Finset.coe_image` `threeAPFree` `subset` `Set.BijOn.mapsTo` `Set.SurjOn.bijOn_subset` `Set.BijOn.injOn` `SetLike.coe_subset_coe` `instIsConcreteLE`
`threeAPFree` 📖	—	`IsAddFreimanHom` `Set.InjOn` `ThreeAPFree` `AddCommMonoid.toAddMonoid`	—	—	`ThreeAPFree.of_image` `subset_rfl` `Set.instReflSubset` `ThreeAPFree.mono` `Set.MapsTo.image_subset` `mapsTo`

IsAddFreimanIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addRothNumber_congr` 📖	mathematical	`IsAddFreimanIso` `SetLike.coe` `Finset` `Finset.instSetLike`	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `AddCommMonoid.toAddMonoid`	—	`le_antisymm` `addRothNumber_spec` `Set.InjOn.mono` `Finset.coe_subset` `Set.BijOn.injOn` `bijOn` `threeAPFree_congr` `subset` `Set.InjOn.bijOn_image` `Finset.card_image_of_injOn` `ThreeAPFree.le_addRothNumber` `Finset.coe_image` `Set.MapsTo.image_subset` `Set.MapsTo.mono` `Set.BijOn.mapsTo` `Finset.Subset.rfl` `IsAddFreimanHom.addRothNumber_mono` `isAddFreimanHom`
`threeAPFree_congr` 📖	mathematical	`IsAddFreimanIso`	`ThreeAPFree` `AddCommMonoid.toAddMonoid`	—	`threeAPFree_image` `subset_rfl` `Set.instReflSubset` `Set.BijOn.image_eq` `bijOn`

IsMulFreimanHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulRothNumber_mono` 📖	mathematical	`IsMulFreimanHom` `SetLike.coe` `Finset` `Finset.instSetLike` `Set.BijOn`	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `CommMonoid.toMonoid`	—	`mulRothNumber_spec` `One.instNonempty` `Set.MapsTo.image_subset` `Set.MapsTo.mono` `Set.SurjOn.mapsTo_invFunOn` `Set.BijOn.surjOn` `Finset.coe_subset` `Finset.Subset.rfl` `Set.SurjOn.mono` `Finset.card_image_of_injOn` `Set.InjOn.mono` `Function.invFunOn_injOn_image` `ThreeGPFree.le_mulRothNumber` `Finset.coe_image` `threeGPFree` `subset` `Set.BijOn.mapsTo` `Set.SurjOn.bijOn_subset` `Set.BijOn.injOn` `instIsConcreteLE`
`threeGPFree` 📖	—	`IsMulFreimanHom` `Set.InjOn` `ThreeGPFree` `CommMonoid.toMonoid`	—	—	`ThreeGPFree.of_image` `subset_rfl` `Set.instReflSubset` `ThreeGPFree.mono` `Set.MapsTo.image_subset` `mapsTo`

IsMulFreimanIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulRothNumber_congr` 📖	mathematical	`IsMulFreimanIso` `SetLike.coe` `Finset` `Finset.instSetLike`	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `CommMonoid.toMonoid`	—	`le_antisymm` `mulRothNumber_spec` `Set.InjOn.mono` `Finset.coe_subset` `Set.BijOn.injOn` `bijOn` `threeGPFree_congr` `subset` `Set.InjOn.bijOn_image` `Finset.card_image_of_injOn` `ThreeGPFree.le_mulRothNumber` `Finset.coe_image` `Set.MapsTo.image_subset` `Set.MapsTo.mono` `Set.BijOn.mapsTo` `Finset.Subset.rfl` `IsMulFreimanHom.mulRothNumber_mono` `isMulFreimanHom`
`threeGPFree_congr` 📖	mathematical	`IsMulFreimanIso`	`ThreeGPFree` `CommMonoid.toMonoid`	—	`threeGPFree_image` `subset_rfl` `Set.instReflSubset` `Set.BijOn.image_eq` `bijOn`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`threeAPFree` 📖	mathematical	`Set.Subsingleton`	`ThreeAPFree`	—	—
`threeGPFree` 📖	mathematical	`Set.Subsingleton`	`ThreeGPFree`	—	—

ThreeAPFree

Definitions

Name	Category	Theorems
`instDecidable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addRothNumber_eq` 📖	mathematical	`ThreeAPFree` `SetLike.coe` `Finset` `Finset.instSetLike`	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `Finset.card`	—	`LE.le.antisymm` `addRothNumber_le` `le_addRothNumber` `Finset.Subset.refl`
`eq_right` 📖	—	`ThreeAPFree` `AddCommMonoid.toAddMonoid` `Set` `Set.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—	`IsCancelAdd.toIsLeftCancelAdd`
`image` 📖	mathematical	`IsAddFreimanIso` `Set` `Set.instHasSubset` `ThreeAPFree` `AddCommMonoid.toAddMonoid`	`Set.image`	—	`threeAPFree_image`
`image'` 📖	mathematical	`Set.InjOn` `DFunLike.coe` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `ThreeAPFree`	`Set.image`	—	`Set.add_mem_add` `map_add`
`le_addRothNumber` 📖	mathematical	`ThreeAPFree` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.instHasSubset`	`Finset.card` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber`	—	`Nat.le_findGreatest` `Finset.card_le_card`
`le_rothNumberNat` 📖	mathematical	`ThreeAPFree` `Nat.instAddMonoid` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.card`	`DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `rothNumberNat`	—	`LE.le.trans` `Eq.ge` `le_addRothNumber` `Finset.mem_range`
`mono` 📖	—	`Set` `Set.instHasSubset` `ThreeAPFree`	—	—	—
`of_image` 📖	—	`IsAddFreimanHom` `Set.InjOn` `Set` `Set.instHasSubset` `ThreeAPFree` `AddCommMonoid.toAddMonoid` `Set.image`	—	—	`Set.mem_image_of_mem` `IsAddFreimanHom.add_eq_add`
`prod` 📖	mathematical	`ThreeAPFree`	`Prod.instAddMonoid` `SProd.sprod` `Set` `Set.instSProd`	—	—
`vadd_set` 📖	mathematical	`ThreeAPFree` `AddCommMonoid.toAddMonoid`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`add_add_add_comm` `IsCancelAdd.toIsLeftCancelAdd`

ThreeGPFree

Definitions

Name	Category	Theorems
`instDecidable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_right` 📖	—	`ThreeGPFree` `CommMonoid.toMonoid` `Set` `Set.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—	`IsCancelMul.toIsLeftCancelMul`
`image` 📖	mathematical	`IsMulFreimanIso` `Set` `Set.instHasSubset` `ThreeGPFree` `CommMonoid.toMonoid`	`Set.image`	—	`threeGPFree_image`
`image'` 📖	mathematical	`Set.InjOn` `DFunLike.coe` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `ThreeGPFree`	`Set.image`	—	`Set.mul_mem_mul` `map_mul`
`le_mulRothNumber` 📖	mathematical	`ThreeGPFree` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.instHasSubset`	`Finset.card` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber`	—	`Nat.le_findGreatest` `Finset.card_le_card`
`mono` 📖	—	`Set` `Set.instHasSubset` `ThreeGPFree`	—	—	—
`mulRothNumber_eq` 📖	mathematical	`ThreeGPFree` `SetLike.coe` `Finset` `Finset.instSetLike`	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `Finset.card`	—	`LE.le.antisymm` `mulRothNumber_le` `le_mulRothNumber` `Finset.Subset.refl`
`of_image` 📖	—	`IsMulFreimanHom` `Set.InjOn` `Set` `Set.instHasSubset` `ThreeGPFree` `CommMonoid.toMonoid` `Set.image`	—	—	`Set.mem_image_of_mem` `IsMulFreimanHom.mul_eq_mul`
`prod` 📖	mathematical	`ThreeGPFree`	`Prod.instMonoid` `SProd.sprod` `Set` `Set.instSProd`	—	—
`smul_set` 📖	mathematical	`ThreeGPFree` `CommMonoid.toMonoid`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`mul_mul_mul_comm` `IsCancelMul.toIsLeftCancelMul`
`smul_set₀` 📖	mathematical	`ThreeGPFree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Set` `Set.smulSet` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero`	—	`mul_mul_mul_comm` `IsCancelMulZero.toIsLeftCancelMulZero`

(root)

Definitions

Name	Category	Theorems
`ThreeAPFree` 📖	MathDef	17 math math: `roth_3ap_theorem`, `rothNumberNat_spec`, `threeAPFree_sphere`, `threeAPFree_vadd_set`, `threeAPFree_iff_eq_right`, `threeAPFree_frontier`, `addRothNumber_spec`, `threeAPFree_singleton`, `roth_3ap_theorem_nat`, `threeAPFree_empty`, `threeAPFree_image`, `IsAddFreimanIso.threeAPFree_congr`, `Set.Subsingleton.threeAPFree`, `Behrend.threeAPFree_image_sphere`, `Behrend.threeAPFree_sphere`, `threeAPFree_insert`, `threeAPFree_insert_of_lt`
`ThreeGPFree` 📖	MathDef	10 math math: `mulRothNumber_spec`, `threeGPFree_empty`, `threeGPFree_smul_set`, `threeGPFree_insert`, `threeGPFree_insert_of_lt`, `threeGPFree_singleton`, `Set.Subsingleton.threeGPFree`, `threeGPFree_image`, `threeGPFree_smul_set₀`, `IsMulFreimanIso.threeGPFree_congr`
`addRothNumber` 📖	CompOp	18 math math: `le_addRothNumber_product`, `ThreeAPFree.addRothNumber_eq`, `addRothNumber_union_le`, `Fin.addRothNumber_eq_rothNumberNat`, `addRothNumber_spec`, `addRothNumber_le_ruzsaSzemerediNumber`, `addRothNumber_empty`, `rothNumberNat_def`, `addRothNumber_lt_of_forall_not_threeAPFree`, `addRothNumber_singleton`, `ThreeAPFree.le_addRothNumber`, `addRothNumber_map_add_left`, `Fin.addRothNumber_le_rothNumberNat`, `IsAddFreimanIso.addRothNumber_congr`, `addRothNumber_le`, `IsAddFreimanHom.addRothNumber_mono`, `addRothNumber_Ico`, `addRothNumber_map_add_right`
`mulRothNumber` 📖	CompOp	13 math math: `mulRothNumber_map_mul_left`, `mulRothNumber_spec`, `IsMulFreimanHom.mulRothNumber_mono`, `ThreeGPFree.le_mulRothNumber`, `IsMulFreimanIso.mulRothNumber_congr`, `le_mulRothNumber_product`, `mulRothNumber_empty`, `ThreeGPFree.mulRothNumber_eq`, `mulRothNumber_le`, `mulRothNumber_lt_of_forall_not_threeGPFree`, `mulRothNumber_map_mul_right`, `mulRothNumber_union_le`, `mulRothNumber_singleton`
`rothNumberNat` 📖	CompOp	17 math math: `Behrend.roth_lower_bound`, `rothNumberNat_spec`, `Behrend.roth_lower_bound_explicit`, `rothNumberNat_le`, `Behrend.bound_aux'`, `rothNumberNat_zero`, `Fin.addRothNumber_eq_rothNumberNat`, `rothNumberNat_def`, `rothNumberNat_isLittleO_id`, `ThreeAPFree.le_rothNumberNat`, `Behrend.card_sphere_le_rothNumberNat`, `rothNumberNat_le_ruzsaSzemerediNumberNat`, `rothNumberNat_add_le`, `Fin.addRothNumber_le_rothNumberNat`, `Behrend.bound_aux`, `addRothNumber_Ico`, `rothNumberNat_le_ruzsaSzemerediNumberNat'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addRothNumber_Ico` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `Nat.instAddMonoid` `Finset.Ico` `Nat.instLocallyFiniteOrder` `rothNumberNat`	—	`le_total` `Finset.Ico_eq_empty_of_le` `rothNumberNat_zero` `addRothNumber_empty` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.range_eq_Ico` `Finset.map_eq_image` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `Finset.image_add_left_Ico` `Nat.instIsOrderedCancelAddMonoid` `addRothNumber_map_add_left`
`addRothNumber_empty` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `Finset.instEmptyCollection`	—	`LE.le.trans` `addRothNumber_le` `Eq.le` `Finset.card_empty`
`addRothNumber_le` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `Finset.card`	—	`Nat.findGreatest_le`
`addRothNumber_lt_of_forall_not_threeAPFree` 📖	mathematical	`ThreeAPFree` `SetLike.coe` `Finset` `Finset.instSetLike`	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber`	—	`addRothNumber_spec` `not_le` `Finset.exists_subset_card_eq` `Finset.mem_powersetCard` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `ThreeAPFree.mono`
`addRothNumber_map_add_left` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Finset.map` `addLeftEmbedding` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AddLeftCancelMonoid.toAddLeftCancelSemigroup` `AddCancelCommMonoid.toAddLeftCancelMonoid`	—	`le_antisymm` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `addRothNumber_spec` `Finset.subset_map_iff` `Finset.card_map` `ThreeAPFree.le_addRothNumber` `threeAPFree_vadd_set` `AddCancelMonoid.toIsCancelAdd` `Finset.coe_map` `ThreeAPFree.vadd_set` `Finset.map_subset_map`
`addRothNumber_map_add_right` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Finset.map` `addRightEmbedding` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `IsCancelAdd.toIsLeftCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsCancelAdd.toIsRightCancelAdd` `addLeftEmbedding_eq_addRightEmbedding` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `addRothNumber_map_add_left`
`addRothNumber_singleton` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `Finset.instSingleton`	—	`ThreeAPFree.addRothNumber_eq` `Finset.coe_singleton` `threeAPFree_singleton`
`addRothNumber_spec` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finset.card` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `ThreeAPFree` `SetLike.coe` `Finset.instSetLike`	—	`Nat.findGreatest_spec` `Finset.empty_subset` `Finset.card_empty` `Finset.coe_empty` `threeAPFree_empty`
`addRothNumber_union_le` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `Finset.instUnion`	—	`addRothNumber_spec` `Finset.inter_union_distrib_left` `Finset.inter_eq_left` `Finset.card_union_le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `ThreeAPFree.le_addRothNumber` `ThreeAPFree.mono` `Finset.inter_subset_left` `Finset.inter_subset_right`
`le_addRothNumber_product` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `Prod.instAddMonoid` `SProd.sprod` `Finset.instSProd`	—	`addRothNumber_spec` `Finset.card_product` `ThreeAPFree.le_addRothNumber` `Finset.coe_product` `ThreeAPFree.prod` `Finset.product_subset_product`
`le_mulRothNumber_product` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `Prod.instMonoid` `SProd.sprod` `Finset.instSProd`	—	`mulRothNumber_spec` `Finset.card_product` `ThreeGPFree.le_mulRothNumber` `Finset.coe_product` `ThreeGPFree.prod` `Finset.product_subset_product`
`mulRothNumber_empty` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `Finset.instEmptyCollection`	—	`LE.le.trans` `mulRothNumber_le` `Eq.le` `Finset.card_empty`
`mulRothNumber_le` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `Finset.card`	—	`Nat.findGreatest_le`
`mulRothNumber_lt_of_forall_not_threeGPFree` 📖	mathematical	`ThreeGPFree` `SetLike.coe` `Finset` `Finset.instSetLike`	`DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber`	—	`mulRothNumber_spec` `not_le` `Finset.exists_subset_card_eq` `Finset.mem_powersetCard` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `ThreeGPFree.mono`
`mulRothNumber_map_mul_left` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `CommMonoid.toMonoid` `CancelCommMonoid.toCommMonoid` `Finset.map` `mulLeftEmbedding` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `LeftCancelSemigroup.toIsLeftCancelMul` `LeftCancelMonoid.toLeftCancelSemigroup` `CancelCommMonoid.toLeftCancelMonoid`	—	`le_antisymm` `LeftCancelSemigroup.toIsLeftCancelMul` `mulRothNumber_spec` `Finset.subset_map_iff` `Finset.card_map` `ThreeGPFree.le_mulRothNumber` `threeGPFree_smul_set` `CancelMonoid.toIsCancelMul` `Finset.coe_map` `ThreeGPFree.smul_set` `Finset.map_subset_map`
`mulRothNumber_map_mul_right` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `CommMonoid.toMonoid` `CancelCommMonoid.toCommMonoid` `Finset.map` `mulRightEmbedding` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelSemigroup.toIsRightCancelMul` `RightCancelMonoid.toRightCancelSemigroup` `CancelMonoid.toRightCancelMonoid` `CancelCommMonoid.toCancelMonoid`	—	`RightCancelSemigroup.toIsRightCancelMul` `IsCancelMul.toIsLeftCancelMul` `CancelMonoid.toIsCancelMul` `IsCancelMul.toIsRightCancelMul` `mulLeftEmbedding_eq_mulRightEmbedding` `LeftCancelSemigroup.toIsLeftCancelMul` `mulRothNumber_map_mul_left`
`mulRothNumber_singleton` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `Finset.instSingleton`	—	`ThreeGPFree.mulRothNumber_eq` `Finset.coe_singleton` `threeGPFree_singleton`
`mulRothNumber_spec` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finset.card` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `ThreeGPFree` `SetLike.coe` `Finset.instSetLike`	—	`Nat.findGreatest_spec` `Finset.empty_subset` `Finset.card_empty` `Finset.coe_empty` `threeGPFree_empty`
`mulRothNumber_union_le` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `mulRothNumber` `Finset.instUnion`	—	`mulRothNumber_spec` `Finset.inter_union_distrib_left` `Finset.inter_eq_left` `Finset.card_union_le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `ThreeGPFree.le_mulRothNumber` `ThreeGPFree.mono` `Finset.inter_subset_left` `Finset.inter_subset_right`
`rothNumberNat_add_le` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `rothNumberNat`	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.range_add_eq_union` `addRothNumber_map_add_left` `addRothNumber_union_le`
`rothNumberNat_def` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `rothNumberNat` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `addRothNumber` `Nat.instAddMonoid` `Finset.range`	—	—
`rothNumberNat_le` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `rothNumberNat`	—	`LE.le.trans` `addRothNumber_le` `Eq.le` `Finset.card_range`
`rothNumberNat_spec` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finset.range` `Finset.card` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `rothNumberNat` `ThreeAPFree` `Nat.instAddMonoid` `SetLike.coe` `Finset.instSetLike`	—	`addRothNumber_spec`
`rothNumberNat_zero` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `rothNumberNat`	—	—
`threeAPFree_empty` 📖	mathematical	—	`ThreeAPFree` `Set` `Set.instEmptyCollection`	—	—
`threeAPFree_iff_eq_right` 📖	mathematical	—	`ThreeAPFree` `Nat.instAddMonoid`	—	`add_left_cancel` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `two_ne_zero` `Nat.instAtLeastTwoHAddOfNat`
`threeAPFree_image` 📖	mathematical	`IsAddFreimanIso` `Set` `Set.instHasSubset`	`ThreeAPFree` `AddCommMonoid.toAddMonoid` `Set.image`	—	`ThreeAPFree.eq_1` `Set.InjOn.bijOn_image` `Set.InjOn.mono` `Set.BijOn.injOn` `IsAddFreimanIso.bijOn` `Set.BijOn.forall` `IsAddFreimanIso.add_eq_add` `Set.InjOn.eq_iff`
`threeAPFree_insert` 📖	mathematical	—	`ThreeAPFree` `AddCommMonoid.toAddMonoid` `Set` `Set.instInsert`	—	`ThreeAPFree.mono` `Set.subset_insert` `Set.mem_insert_iff` `add_right_cancel` `IsCancelAdd.toIsRightCancelAdd` `add_comm`
`threeAPFree_insert_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`ThreeAPFree` `AddCommMonoid.toAddMonoid` `Set` `Set.instInsert`	—	`threeAPFree_insert` `IsOrderedCancelAddMonoid.toIsCancelAdd` `LT.lt.ne` `add_lt_add_of_lt_of_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`threeAPFree_pi` 📖	mathematical	`ThreeAPFree`	`Pi.addMonoid` `Set.pi` `Set.univ`	—	—
`threeAPFree_singleton` 📖	mathematical	—	`ThreeAPFree` `Set` `Set.instSingletonSet`	—	`Set.Subsingleton.threeAPFree` `Set.subsingleton_singleton`
`threeAPFree_vadd_set` 📖	mathematical	—	`ThreeAPFree` `AddCommMonoid.toAddMonoid` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`add_left_cancel` `IsCancelAdd.toIsLeftCancelAdd` `Set.mem_image_of_mem` `add_add_add_comm` `vadd_eq_add` `ThreeAPFree.vadd_set`
`threeGPFree_empty` 📖	mathematical	—	`ThreeGPFree` `Set` `Set.instEmptyCollection`	—	—
`threeGPFree_image` 📖	mathematical	`IsMulFreimanIso` `Set` `Set.instHasSubset`	`ThreeGPFree` `CommMonoid.toMonoid` `Set.image`	—	`ThreeGPFree.eq_1` `Set.InjOn.bijOn_image` `Set.InjOn.mono` `Set.BijOn.injOn` `IsMulFreimanIso.bijOn` `Set.BijOn.forall` `IsMulFreimanIso.mul_eq_mul` `Set.InjOn.eq_iff`
`threeGPFree_insert` 📖	mathematical	—	`ThreeGPFree` `CommMonoid.toMonoid` `Set` `Set.instInsert`	—	`ThreeGPFree.mono` `Set.subset_insert` `Set.mem_insert_iff` `mul_right_cancel` `IsCancelMul.toIsRightCancelMul` `mul_comm`
`threeGPFree_insert_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`ThreeGPFree` `CommMonoid.toMonoid` `Set` `Set.instInsert`	—	`threeGPFree_insert` `IsOrderedCancelMonoid.toIsCancelMul` `LT.lt.ne` `mul_lt_mul_of_lt_of_lt` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `IsCancelMul.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `IsCancelMul.toIsRightCancelMul` `covariant_swap_mul_of_covariant_mul`
`threeGPFree_pi` 📖	mathematical	`ThreeGPFree`	`Pi.monoid` `Set.pi` `Set.univ`	—	—
`threeGPFree_singleton` 📖	mathematical	—	`ThreeGPFree` `Set` `Set.instSingletonSet`	—	`Set.Subsingleton.threeGPFree` `Set.subsingleton_singleton`
`threeGPFree_smul_set` 📖	mathematical	—	`ThreeGPFree` `CommMonoid.toMonoid` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`mul_left_cancel` `IsCancelMul.toIsLeftCancelMul` `Set.mem_image_of_mem` `mul_mul_mul_comm` `smul_eq_mul` `ThreeGPFree.smul_set`
`threeGPFree_smul_set₀` 📖	mathematical	—	`ThreeGPFree` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero`	—	`mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `Set.mem_image_of_mem` `smul_eq_mul` `mul_mul_mul_comm` `ThreeGPFree.smul_set₀`

---

← Back to Index