Star

📁 Source: Mathlib/Data/Int/Star.lean

Statistics

Metric	Count
Definitions	0
Theorems addSubmonoid_closure_range_mul_self, addSubmonoid_closure_range_pow, instStarOrderedRing	3
Total	3

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubmonoid_closure_range_mul_self 📖	mathematical	—	AddSubmonoid.closure AddMonoid.toAddZeroClass instAddMonoid Set.range AddSubmonoid.nonneg PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instAddLeftMono	—	Nat.instAtLeastTwoHAddOfNat instAddLeftMono sq addSubmonoid_closure_range_pow even_two
addSubmonoid_closure_range_pow 📖	mathematical	Even	AddSubmonoid.closure AddMonoid.toAddZeroClass instAddMonoid Set.range Monoid.toNatPow instMonoid AddSubmonoid.nonneg PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instAddLeftMono	—	le_antisymm instAddLeftMono AddSubmonoid.closure_le Set.range_subset_iff Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing AddGroup.existsAddOfLE one_pow Nat.cast_natAbs mul_one instIsOrderedAddMonoid nsmul_mem AddSubmonoid.instAddSubmonoidClass AddSubmonoid.subset_closure Set.mem_range_self
instStarOrderedRing 📖	mathematical	—	StarOrderedRing NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing instCommRing SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instStarRing	—	le_iff_exists_nonneg_add AddGroup.existsAddOfLE instAddLeftMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le TrivialStar.star_trivial instTrivialStar addSubmonoid_closure_range_mul_self

---

← Back to Index