Documentation Verification Report

FrobeniusNumber

📁 Source: Mathlib/NumberTheory/FrobeniusNumber.lean

Statistics

Metric	Count
Definitions `FrobeniusNumber`, `setGcd`	2
Theorems `addSubmonoid_fg`, `dvdNotUnit_setGcd_insert`, `dvd_setGcd_iff`, `exists_mem_closure_of_ge`, `exists_mem_span_nat_finset_of_ge`, `exists_ne_zero_of_setGcd_ne_zero`, `finite_setOf_setGcd_dvd_and_mem_span`, `instIsNoetherian`, `setGcd_dvd_of_mem`, `setGcd_dvd_of_mem_closure`, `setGcd_eq_zero_iff`, `setGcd_insert_of_dvd`, `setGcd_mono`, `span_singleton_setGcd`, `subset_span_setGcd`, `exists_frobeniusNumber_iff`, `frobeniusNumber_iff`, `frobeniusNumber_pair`	18
Total	20

Nat

Definitions

Name	Category	Theorems
`setGcd` 📖	CompOp	9 math math: `subset_span_setGcd`, `setGcd_eq_zero_iff`, `setGcd_dvd_of_mem_closure`, `finite_setOf_setGcd_dvd_and_mem_span`, `exists_frobeniusNumber_iff`, `setGcd_dvd_of_mem`, `dvd_setGcd_iff`, `span_singleton_setGcd`, `setGcd_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubmonoid_fg` 📖	mathematical	—	`AddSubmonoid.FG` `instAddMonoid`	—	`AddSubmonoid.toNatSubmodule_toAddSubmonoid` `Submodule.fg_iff_addSubmonoid_fg` `IsNoetherian.noetherian` `instIsNoetherian`
`dvdNotUnit_setGcd_insert` 📖	mathematical	`setGcd`	`DvdNotUnit` `instCommMonoidWithZero` `Set` `Set.instInsert`	—	`dvdNotUnit_of_dvd_of_not_dvd` `setGcd_mono` `Set.subset_insert` `dvd_setGcd_iff` `Set.mem_insert`
`dvd_setGcd_iff` 📖	mathematical	—	`setGcd`	—	—
`exists_mem_closure_of_ge` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `instAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure`	—	`exists_mem_span_nat_finset_of_ge` `Eq.le` `Submodule.span_nat_eq_addSubmonoidClosure` `Submodule.span_mono`
`exists_mem_span_nat_finset_of_ge` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Ideal` `instSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span`	—	`Finset.coe_empty` `zero_dvd_iff` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Submodule.mem_span_image_iff_exists_fun` `Ideal.mem_span_singleton_self` `span_singleton_setGcd` `exists_ne_zero_of_setGcd_ne_zero` `Finset.coe_insert` `ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `add_comm` `add_assoc` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Ideal.mul_mem_left` `Ideal.subset_span` `Finset.mem_insert_self` `Submodule.span_mono` `Finset.subset_insert` `setGcd_dvd_of_mem` `dvd_mul_of_dvd_right` `Finset.dvd_sum` `Finset.mul_sum` `mul_comm` `cast_add` `cast_sum` `cast_mul` `Finset.sum_congr` `Distrib.rightDistribClass` `cast_zero` `MulZeroClass.mul_zero` `add_zero` `Int.natCast_natAbs` `abs_eq_self` `Int.instIsOrderedAddMonoid` `cast_sub` `pos_of_ne_zero` `LT.lt.le` `abs_eq_neg_self` `sub_mul` `mul_neg` `sub_neg_eq_add` `sum_mem`
`exists_ne_zero_of_setGcd_ne_zero` 📖	mathematical	—	`Set` `Set.instMembership`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `setGcd_eq_zero_iff`
`finite_setOf_setGcd_dvd_and_mem_span` 📖	mathematical	—	`Set.Finite` `setOf` `setGcd` `Ideal` `instSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span`	—	`exists_mem_closure_of_ge` `Set.Finite.subset` `Finset.finite_toSet` `Finset.mem_range` `lt_of_not_ge` `Eq.ge` `Submodule.span_nat_eq_addSubmonoidClosure`
`instIsNoetherian` 📖	mathematical	—	`IsNoetherian` `instSemiring` `instAddCommMonoid` `AddCommMonoid.toNatModule`	—	`exists_mem_span_nat_finset_of_ge` `LE.le.antisymm` `Submodule.span_le` `Finset.coe_union` `Finset.coe_filter` `le_or_gt` `Submodule.span_mono` `setGcd_dvd_of_mem` `Submodule.subset_span`
`setGcd_dvd_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`setGcd`	—	`setGcd.eq_1` `Int.dvd_natCast` `Submodule.IsPrincipal.mem_iff_generator_dvd` `Ideal.subset_span`
`setGcd_dvd_of_mem_closure` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `instAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure`	`setGcd`	—	`AddSubmonoid.closure_induction` `setGcd_dvd_of_mem` `dvd_zero` `dvd_add` `Distrib.leftDistribClass`
`setGcd_eq_zero_iff` 📖	mathematical	—	`setGcd` `Set` `Set.instHasSubset` `Set.instSingletonSet`	—	—
`setGcd_insert_of_dvd` 📖	mathematical	`setGcd`	`Set` `Set.instInsert`	—	`Dvd.dvd.antisymm` `instIsCancelMulZero` `Unique.instSubsingleton` `setGcd_mono` `Set.subset_insert` `dvd_setGcd_iff` `setGcd_dvd_of_mem`
`setGcd_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`setGcd`	—	`dvd_setGcd_iff` `setGcd_dvd_of_mem`
`span_singleton_setGcd` 📖	mathematical	—	`Ideal.span` `Int.instSemiring` `Set` `Set.instSingletonSet` `setGcd` `Set.image`	—	`setGcd.eq_1` `Ideal.span_singleton_eq_span_singleton` `Int.instIsDomain` `Int.associated_natAbs` `Ideal.span.eq_1` `Submodule.IsPrincipal.span_singleton_generator`
`subset_span_setGcd` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `instSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span` `Set.instSingletonSet` `setGcd`	—	`Ideal.mem_span_singleton` `setGcd_dvd_of_mem`

(root)

Definitions

Name	Category	Theorems
`FrobeniusNumber` 📖	MathDef	3 math math: `frobeniusNumber_pair`, `frobeniusNumber_iff`, `exists_frobeniusNumber_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_frobeniusNumber_iff` 📖	mathematical	—	`FrobeniusNumber` `Nat.setGcd` `Set` `Set.instMembership`	—	`Nat.setGcd_dvd_of_mem_closure` `frobeniusNumber_iff` `AddSubmonoid.closure_mono` `Set.singleton_subset_iff` `Eq.ge` `Nat.addSubmonoidClosure_one` `Nat.exists_mem_closure_of_ge` `Nat.one_mem_closure_iff` `Nat.findGreatest_spec` `le_of_not_gt` `LT.lt.le` `Eq.dvd` `le_total` `of_not_not` `Nat.findGreatest_is_greatest` `Dvd.dvd.trans` `one_dvd`
`frobeniusNumber_iff` 📖	mathematical	—	`FrobeniusNumber` `AddSubmonoid` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure`	—	—
`frobeniusNumber_pair` 📖	mathematical	—	`FrobeniusNumber` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`add_le_mul` `Nat.instZeroLEOneClass` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.instIsStrictOrderedRing` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.Coprime.mul_add_mul_ne_mul` `Nat.cast_add` `Nat.cast_mul` `Nat.cast_one` `sub_eq_zero` `Nat.cast_sub` `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.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.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Contrapose.contrapose₂` `Nat.chineseRemainder_lt_mul` `ne_bot_of_gt` `Nat.ModEq.le_of_lt_add` `lt_of_le_of_lt` `le_tsub_of_add_le_left` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.ModEq.trans` `Nat.ModEq.symm` `Nat.modEq_zero_iff_dvd` `dvd_mul_right` `dvd_rfl` `lt_of_lt_of_le` `le_tsub_add` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Nat.modEq_iff_dvd'` `mul_comm`

---

← Back to Index