Star

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

Statistics

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

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubmonoid_closure_range_mul_self 📖	mathematical	—	AddSubmonoid.closure NNRat AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield Set.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Top.top AddSubmonoid AddSubmonoid.instTop	—	sq addSubmonoid_closure_range_pow two_ne_zero
addSubmonoid_closure_range_pow 📖	mathematical	—	AddSubmonoid.closure NNRat AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield Set.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Top.top AddSubmonoid AddSubmonoid.instTop	—	AddSubmonoid.eq_top_iff' nsmul_eq_mul Nat.cast_mul Nat.cast_pow mul_assoc pow_sub₀ instCharZero LT.lt.ne' den_pos pow_one mul_right_comm mul_pow mul_inv_cancel₀ one_pow one_mul div_eq_mul_inv num_div_den nsmul_mem AddSubmonoid.instAddSubmonoidClass AddSubmonoid.subset_closure Set.mem_range_self
instStarOrderedRing 📖	mathematical	—	StarOrderedRing NNRat NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring instCommSemiringNNRat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat instStarRing	—	le_iff_exists_nonneg_add CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le TrivialStar.star_trivial instTrivialStar addSubmonoid_closure_range_mul_self

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubmonoid_closure_range_mul_self 📖	mathematical	—	AddSubmonoid.closure AddMonoid.toAddZeroClass addMonoid Set.range AddSubmonoid.nonneg instPreorder instAddLeftMono	—	instAddLeftMono sq addSubmonoid_closure_range_pow two_ne_zero even_two
addSubmonoid_closure_range_pow 📖	mathematical	Even	AddSubmonoid.closure AddMonoid.toAddZeroClass addMonoid Set.range AddSubmonoid.nonneg instPreorder instAddLeftMono	—	instAddLeftMono RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Even.pow_abs IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing Set.image_congr eq_nnratCast Set.instReflSubset Set.instAntisymmSubset AddSubmonoid.ext AddSubmonoid.map.congr_simp NNRat.addSubmonoid_closure_range_pow AddMonoidHom.map_mclosure
instStarOrderedRing 📖	mathematical	—	StarOrderedRing NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing instPartialOrder 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