Kleene

📁 Source: Mathlib/Algebra/Order/Kleene.lean

Statistics

Metric	Count
Definitions «term_∗», idemCommSemiring, idemSemiring, kleeneAlgebra, IdemCommSemiring, bot, toCommSemiring, toIdemSemiring, toSemilatticeSup, IdemSemiring, bot, ofSemiring, toOrderBot, toSemilatticeSup, toSemiring, KStar, kstar, KleeneAlgebra, toIdemSemiring, toKStar, instIdemCommSemiringForall, instIdemSemiring, instKleeneAlgebraForall, instIdemCommSemiring, instIdemSemiring, instKleeneAlgebra	26
Theorems add_eq_sup, bot_le, add_eq_sup, bot_le, toCanonicallyOrderedAdd, toIsOrderedAddMonoid, toMulLeftMono, toMulRightMono, kstar_mul_le_kstar, kstar_mul_le_self, mul_kstar_le_kstar, mul_kstar_le_self, one_le_kstar, add_eq_left, add_eq_right, kstar_apply, kstar_def, fst_kstar, kstar_def, snd_kstar, add_eq_left_iff_le, add_eq_right_iff_le, add_eq_sup, add_idem, add_le, add_le_iff, kstar_eq_one, kstar_eq_self, kstar_idem, kstar_le_of_mul_le_left, kstar_le_of_mul_le_right, kstar_mono, kstar_mul_kstar, kstar_mul_le, kstar_mul_le_kstar, kstar_mul_le_self, kstar_one, kstar_zero, le_kstar, mul_kstar_le, mul_kstar_le_kstar, mul_kstar_le_self, natCast_eq_one, nsmul_eq_self, ofNat_eq_one, one_le_kstar, pow_le_kstar	47
Total	73

Computability

Definitions

Name	Category	Theorems
«term_∗» 📖	CompOp	—

Function.Injective

Definitions

Name	Category	Theorems
idemCommSemiring 📖	CompOp	—
idemSemiring 📖	CompOp	—
kleeneAlgebra 📖	CompOp	—

IdemCommSemiring

Definitions

Name	Category	Theorems
bot 📖	CompOp	1 math math: bot_le
toCommSemiring 📖	CompOp	105 math math: FractionalIdeal.finprod_heightOneSpectrum_factorization_principal, NumberField.isCoprime_differentIdeal_of_isCoprime_discr, Submodule.isInternal_prime_power_torsion_of_pid, Submodule.coe_mapAlgEquiv_symm_apply, Ideal.prime_of_mem_primesOver, Associates.finite_factors, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, Ideal.IsPrime.prod_le, FractionalIdeal.count_well_defined, Ideal.isPrime_iff_bot_or_prime, Ideal.Factors.fact_ramificationIdx_neZero, prod_normalizedFactors_eq_self, IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg, Ideal.count_normalizedFactors_eq, Ideal.gcd_eq_sup, Ideal.prime_span_singleton_iff, Ideal.prod_le_inf, Ideal.isCoprime_iff_gcd, Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal, Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, FractionalIdeal.finprod_heightOneSpectrum_factorization, normalizedFactorsEquivOfQuotEquiv_symm, Ideal.IsPrime.multiset_prod_map_le, instWfDvdMonoidIdeal, FractionalIdeal.count_ne_zero, Ideal.multiset_prod_span_singleton, Ideal.Factors.isScalarTower, Associates.le_singleton_iff, Submodule.prod_span, Submodule.prod_span_singleton, IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime, Submodule.coe_mapAlgEquiv_apply, IsDedekindDomain.HeightOneSpectrum.prime, Ideal.IsPrime.multiset_prod_le, count_span_normalizedFactors_eq_of_normUnit, irreducible_pow_sup, Ideal.isCoprime_tfae, PrimeSpectrum.exists_primeSpectrum_prod_le, Submodule.unitsQuotEquivRelPic_symm_apply, Ideal.prod_mem_prod, Ideal.finite_mulSupport_coe, Ideal.mem_normalizedFactors_iff, Ideal.Factors.liesOver, Ideal.isCoprime_iff_exists, count_le_of_ideal_ge, ClassGroup.equivPic_symm_apply, IsDedekindDomain.HeightOneSpectrum.intValuation_def, Ideal.prime_iff_isPrime, Ideal.coprime_of_no_prime_ge, Ideal.Factors.finrank_pow_ramificationIdx, Ideal.mem_primesOver_iff_mem_normalizedFactors, Ideal.count_associates_eq, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity, Ideal.map_algebraMap_eq_finset_prod_pow, count_span_normalizedFactors_eq, Ideal.factors_span_eq, Ideal.prod_span, Submodule.isInternal_prime_power_torsion, Ideal.finprod_count, Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count, Ideal.sup_prod_eq_top, Ideal.uniqueFactorizationMonoid, IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count, Ideal.isCoprime_span_singleton_iff, Ideal.lcm_eq_inf, Ideal.isCoprime_iff_add, Ideal.eq_prime_pow_mul_coprime, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, Ideal.Factors.finiteDimensional_quotient_pow, Ideal.finprod_heightOneSpectrum_factorization_coe, exists_multiset_prod_cons_le_and_prod_not_le, FractionalIdeal.finite_factors', count_associates_factors_eq, Ideal.multiset_prod_le_inf, Ideal.Factors.isPrime, Ideal.count_associates_eq', Submodule.coe_mapAlgHom_apply, add_eq_sup, sup_eq_prod_inf_factors, Ideal.multiset_prod_eq_bot, Ideal.prod_span_singleton, Ideal.dvdNotUnit_iff_lt, Ideal.prod_sup_eq_top, Ideal.isCoprime_iff_codisjoint, Ideal.isCoprime_iff_sup_eq, Ideal.prime_of_isPrime, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction, Ideal.isCoprime_of_isMaximal, Ideal.Factors.piQuotientEquiv_mk, Ideal.finprod_not_dvd, IsDedekindDomain.HeightOneSpectrum.associates_irreducible, Ideal.finite_quotient_prod, PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain, Ideal.finite_mulSupport_inv, IsDedekindDomain.quotientEquivPiFactors_mk, singleton_span_mem_normalizedFactors_of_mem_normalizedFactors, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, Ideal.finprod_heightOneSpectrum_factorization, FractionalIdeal.count_coe, Ideal.Factors.piQuotientEquiv_map, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity, Ideal.sup_multiset_prod_eq_top, Submodule.unitsQuotEquivRelPic_apply_coe, FractionalIdeal.coeIdeal_finprod, KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span
toIdemSemiring 📖	CompOp	5 math math: AlgebraicGeometry.Scheme.IdealSheafData.radical_sup, AlgebraicGeometry.Scheme.IdealSheafData.comap_sup, AlgebraicGeometry.Scheme.IdealSheafData.instIsOrderedRing, AlgebraicGeometry.Scheme.IdealSheafData.support_sup, AlgebraicGeometry.Scheme.IdealSheafData.add_eq_sup
toSemilatticeSup 📖	CompOp	2 math math: bot_le, add_eq_sup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_sup 📖	mathematical	—	AddSemigroup.toAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CommSemiring.toSemiring toCommSemiring SemilatticeSup.toMax toSemilatticeSup	—	—
bot_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder toSemilatticeSup bot	—	—

IdemSemiring

Definitions

Name	Category	Theorems
bot 📖	CompOp	1 math math: bot_le
ofSemiring 📖	CompOp	—
toOrderBot 📖	CompOp	—
toSemilatticeSup 📖	CompOp	76 math math: Ideal.radical_sup, DoubleQuot.liftSupQuotQuotMkₐ_toRingHom, AlgebraicGeometry.Scheme.IdealSheafData.radical_sup, add_eq_sup, DoubleQuot.coe_quotLeftToQuotSupₐ, irreducible_pow_sup_of_ge, Ideal.gcd_eq_sup, Ideal.sup_eq_top_iff_isCoprime, Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes, add_eq_left_iff_le, add_eq_sup, DoubleQuot.quotQuotToQuotSupₐ_toRingHom, Ideal.sup_pow_add_le_pow_sup_pow, FractionalIdeal.coeIdeal_sup, PrimeSpectrum.sup_vanishingIdeal_le, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, toMulLeftMono, Algebra.adjoin_nonUnitalSubalgebra_eq_span, IsFractional.sup, Ideal.mem_minimalPrimes_sup, DoubleQuot.ker_quotQuotMk, DoubleQuot.coe_quotQuotEquivQuotSupₐ, KleeneAlgebra.one_le_kstar, one_le_kstar, add_le_iff, AlgebraicGeometry.Scheme.IdealSheafData.comap_sup, DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm, IsCoprime.sup_eq, irreducible_pow_sup, add_eq_right_iff_le, Algebra.Generators.comp_localizationAway_ker, Ideal.iSup_iInf_eq_top_iff_pairwise, Ideal.isCoprime_tfae, DividedPowers.isSubDPIdeal_sup, KleeneAlgebra.mul_kstar_le_kstar, Ideal.sup_mul_inf, DoubleQuot.ker_quotLeftToQuotSup, Ideal.minimalPrimes_map_of_surjective, toCanonicallyOrderedAdd, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, FractionalIdeal.coe_sup, kstar_mono, DoubleQuot.quotQuotEquivQuotSup_quotQuotMk, Algebra.Generators.ker_comp_eq_sup, DoubleQuot.coe_quotQuotToQuotSupₐ, Ideal.map_eq_iff_sup_ker_eq_of_surjective, DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, le_kstar, bot_le, pow_le_kstar, Ideal.eq_prime_pow_mul_coprime, ProjectiveSpectrum.zeroLocus_sup_ideal, DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk, irreducible_pow_sup_of_le, kstar_eq_self, KleeneAlgebra.kstar_mul_le_kstar, sup_eq_prod_inf_factors, MonomialOrder.sPolynomial_mem_sup_ideal, PrimeSpectrum.zeroLocus_sup, DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap, AlgebraicGeometry.Scheme.IdealSheafData.support_sup, Ideal.isCoprime_iff_sup_eq, IsDedekindDomain.exists_sup_span_eq, DoubleQuot.quotLeftToQuotSupₐ_toRingHom, DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv, IsLocalization.coeSubmodule_sup, mul_kstar_le_kstar, DoubleQuot.coe_liftSupQuotQuotMkₐ, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, toMulRightMono, toIsOrderedAddMonoid, kstar_mul_le_kstar, AlgebraicGeometry.Scheme.IdealSheafData.add_eq_sup, kstar_eq_one
toSemiring 📖	CompOp	236 math math: Ideal.toCotangent_to_quotient_square, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal, Ideal.finite_setOf_absNorm_le₀, ClassGroup.mk0_integralRep, add_eq_sup, ClassGroup.mk0_eq_mk0_iff, Ideal.toCotangent_eq, Ideal.absNorm_span_insert, Ideal.squarefree_span_singleton, Ideal.relNorm_smul, FractionalIdeal.coeIdealHom_apply, NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, Submodule.coe_mapAlgEquiv_symm_apply, normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity, LE.le.add_eq_right, SetSemiring.instIsOrderedRing, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, Associates.finite_factors, Ideal.comap_cotangentIdeal, NumberField.FinitePlace.norm_def', Ideal.finite_setOf_absNorm_eq, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, AdicCompletion.incl_apply, FractionalIdeal.count_well_defined, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_apply, Ideal.range_cotangentToQuotientSquare, Ideal.relNorm_mono, FractionalIdeal.absNorm_eq', Ideal.relNorm_relNorm, Ideal.mem_toCotangent_ker, Ideal.absNorm_pos_iff_mem_nonZeroDivisors, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, Submodule.ker_unitsToPic, IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg, Ideal.absNorm_eq_pow_inertiaDeg', Ideal.relNorm_top, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, Ideal.relNorm_eq_pow_of_isPrime_isGalois, Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver, Ideal.absNorm_mem, ofNat_eq_one, IsLocalRing.exists_maximalIdeal_pow_le_of_finite_quotient, Ideal.ramificationIdx_ne_one_iff, Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors, add_eq_left_iff_le, add_eq_sup, IsAdic.hasBasis_nhds, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, Ideal.relNorm_singleton, Ideal.map_relNorm, MvPolynomial.degreesLE_nsmul, Ideal.relNorm_le_comap, FractionalIdeal.finprod_heightOneSpectrum_factorization, IsDedekindDomain.HeightOneSpectrum.irreducible, FractionalIdeal.count_ne_zero, KaehlerDifferential.End_equiv_aux, toMulLeftMono, Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat, natCast_eq_one, FractionalIdeal.canonicalEquiv_mk0, NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow, Associates.le_singleton_iff, Algebra.Extension.Cotangent.mk_eq_zero_iff, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Ideal.exists_relNorm_eq_pow_of_isPrime, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, AdicCompletion.factorₐ_evalₐ_one, Submodule.smul_le_smul, Ideal.span_singleton_nonZeroDivisors, KleeneAlgebra.one_le_kstar, IsAdic.hasBasis_nhds_zero, one_le_kstar, Ideal.relNorm_algebraMap', Submodule.projective_units, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Ideal.mk_mem_cotangentIdeal, Submodule.coe_mapAlgEquiv_apply, Ideal.relNorm_int, Ideal.absNorm_dvd_absNorm_of_le, NumberField.Ideal.tendsto_norm_le_div_atTop₀, MvPolynomial.le_coeffsIn_pow, add_le_iff, Int.absNorm_under_mem, NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, Submodule.singleton_smul, Submodule.unitsToPic_apply, Ideal.spanNorm_eq, FractionalIdeal.absNorm_eq, Submodule.range_unitsToPic, Ideal.relNorm_algebraMap, Submodule.spanSingleton_apply, add_eq_right_iff_le, tensorKaehlerQuotKerSqEquiv_tmul_D, FractionalIdeal.coeSubmoduleHom_apply, Ideal.relNorm_eq_bot_iff, IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one, NumberField.FinitePlace.norm_def_int, Ideal.card_norm_le_eq_card_norm_le_add_one, kstar_mul_kstar, Submodule.unitsQuotEquivRelPic_symm_apply, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_mul, KleeneAlgebra.mul_kstar_le_kstar, ClassGroup.mk_mk0, Ideal.isDomain, Polynomial.isEisensteinAt_iff, NumberField.absNorm_differentIdeal, ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring, Ideal.finite_mulSupport_coe, Ideal.absNorm_top, Ideal.absNorm_apply, Ideal.absNorm_pos_of_nonZeroDivisors, Ideal.toCotangent_eq_zero, KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly, Ideal.cotangentEquivIdeal_apply, Algebra.Extension.Cotangent.mk_eq_mk_iff_sub_mem, toCanonicallyOrderedAdd, nsmul_eq_self, Int.absNorm_under_dvd_absNorm, Algebra.FormallySmooth.iff_split_surjection, ClassGroup.equivPic_symm_apply, Submodule.mker_spanSingleton, IsDedekindDomain.HeightOneSpectrum.intValuation_def, kstar_one, NumberField.exists_ideal_in_class_of_norm_le, Submodule.instInvertibleSubtypeMemVal, NumberField.Ideal.tendsto_norm_le_div_atTop, Ideal.count_associates_eq, Ideal.natAbs_det_equiv, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity, Ideal.absNorm_eq_one_iff, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply, Ideal.radical_pow, Submodule.instIsOrderedRing, MvPolynomial.coeffsIn_pow, Ideal.span_singleton_mem_isPrincipalSubmonoid, IsHausdorff.eq_iff_smodEq, Submodule.mapHom_id, Algebra.Extension.Hom.sub_aux, Ideal.isUnit_iff, ClassGroup.exists_mk0_eq_mk0, Ideal.finite_quotient_pow, IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotient, MvPolynomial.C_mem_pow_idealOfVars_iff, Ideal.finprod_count, ClassGroup.mk0_surjective, Ideal.finite_setOf_absNorm_le, pow_le_kstar, AlgHom.ker_kerSquareLift, Ideal.mem_isPrincipalSubmonoid_iff, ClassGroup.exists_min, NumberField.toNNReal_valued_eq_adicAbv, NumberField.mixedEmbedding.fundamentalCone.preimage_of_IdealSetMap, Units.submodule_isFractional, FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, add_idem, add_le, FractionalIdeal.map_canonicalEquiv_mk0, Ideal.absNorm_eq_pow_inertiaDeg, Ideal.cotangentEquivIdeal_symm_apply, Ideal.finprod_heightOneSpectrum_factorization_coe, AlgebraicGeometry.Scheme.IdealSheafData.instIsOrderedRing, Submodule.mulExact_unitsMap_spanSingleton_unitsToPic, Ideal.absNorm_eq_zero_iff, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, FractionalIdeal.finite_factors', Submodule.setSemiring_smul_def, Submodule.mapHom_apply, Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity, count_associates_factors_eq, Ideal.count_associates_eq', Submodule.coe_mapAlgHom_apply, ClassGroup.equiv_mk0, Ideal.absNorm_bot, Ideal.relNorm_apply, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, kstar_eq_self, KleeneAlgebra.kstar_mul_le_kstar, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply, Int.ideal_span_absNorm_eq_self, Ideal.relNorm_bot, Ideal.norm_mem_relNorm, ClassGroup.mk0_eq_mk0_inv_iff, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_map_one, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, Submodule.span.ringHom_apply, Ideal.absNorm_relNorm, ClassGroup.equivPic_apply, kstar_zero, Int.absNorm_under_eq_sInf, Ideal.absNorm_span_singleton, FractionalIdeal.coeIdeal_absNorm, AlgHom.kerSquareLift_mk, Ideal.map_toCotangent_ker, Ideal.absNorm_algebraMap, Int.cast_mem_ideal_iff, Ideal.relNorm_map_algEquiv, emultiplicity_eq_emultiplicity_span, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction, NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm, Ideal.span_singleton_absNorm_le, Ideal.finprod_not_dvd, Ideal.natAbs_det_basis_change, IsLocalRing.finite_quotient_iff, ClassGroup.integralRep_mem_nonZeroDivisors, Ideal.ringChar_quot, Ideal.cotangentIdeal_square, IsDedekindDomain.HeightOneSpectrum.associates_irreducible, Int.liesOver_span_absNorm, Ideal.finite_mulSupport_inv, Submodule.mulExact_unitsToPic_mapAlgebra, FractionalIdeal.coe_mk0, mul_kstar_le_kstar, Ideal.mapHom_apply, Ideal.relNorm_eq_pow_of_isMaximal, Polynomial.IsEisensteinAt.notMem, Nat.absNorm_under_prime, FractionalIdeal.count_coe, Submodule.ker_unitsMap_spanSingleton, Ideal.relNorm_comap_algEquiv, toMulRightMono, Ideal.to_quotient_square_comp_toCotangent, Submodule.fg_unit, toIsOrderedAddMonoid, kstar_mul_le_kstar, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity, Submodule.unitsQuotEquivRelPic_apply_coe, derivationQuotKerSq_mk, kstar_eq_one, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, LE.le.add_eq_left, Ideal.absNorm_dvd_norm_of_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_sup 📖	mathematical	—	AddSemigroup.toAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring toSemiring SemilatticeSup.toMax toSemilatticeSup	—	—
bot_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder toSemilatticeSup bot	—	—
toCanonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder toSemilatticeSup	—	LE.le.add_eq_right add_eq_left_iff_le add_assoc add_idem add_eq_right_iff_le
toIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toSemiring SemilatticeSup.toPartialOrder toSemilatticeSup	—	add_eq_sup le_imp_le_of_le_of_le sup_le_sup le_refl
toMulLeftMono 📖	mathematical	—	MulLeftMono Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder toSemilatticeSup	—	add_eq_left_iff_le mul_add Distrib.leftDistribClass LE.le.add_eq_left
toMulRightMono 📖	mathematical	—	MulRightMono Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder toSemilatticeSup	—	add_eq_left_iff_le add_mul Distrib.rightDistribClass LE.le.add_eq_left

KStar

Definitions

Name	Category	Theorems
kstar 📖	CompOp	45 math math: Language.map_kstar, Language.join_mem_kstar, Prod.fst_kstar, kstar_le_of_mul_le_left, kstar_idem, NFA.pumping_lemma, Language.self_eq_mul_add_iff, Pi.kstar_apply, Language.one_add_kstar_mul_self_eq_kstar, εNFA.pumping_lemma, Language.one_add_self_mul_kstar_eq_kstar, KleeneAlgebra.mul_kstar_le_self, kstar_mul_le_self, Language.mem_kstar_iff_exists_nonempty, Language.kstar_def, KleeneAlgebra.kstar_mul_le_self, KleeneAlgebra.one_le_kstar, one_le_kstar, kstar_le_of_mul_le_right, RegularExpression.matches'_star, Pi.kstar_def, kstar_mul_kstar, KleeneAlgebra.mul_kstar_le_kstar, mul_kstar_le, Language.kstar_def_nonempty, kstar_one, Prod.snd_kstar, DFA.pumping_lemma, kstar_mono, Prod.kstar_def, le_kstar, pow_le_kstar, Language.nil_mem_kstar, mul_kstar_le_self, kstar_eq_self, KleeneAlgebra.kstar_mul_le_kstar, Language.mul_self_kstar_comm, kstar_zero, kstar_mul_le, Language.reverse_kstar, Language.kstar_eq_iSup_pow, mul_kstar_le_kstar, kstar_mul_le_kstar, Language.mem_kstar, kstar_eq_one

KleeneAlgebra

Definitions

Name	Category	Theorems
toIdemSemiring 📖	CompOp	14 math math: one_le_kstar, one_le_kstar, kstar_mul_kstar, mul_kstar_le_kstar, kstar_one, kstar_mono, le_kstar, pow_le_kstar, kstar_eq_self, kstar_mul_le_kstar, kstar_zero, mul_kstar_le_kstar, kstar_mul_le_kstar, kstar_eq_one
toKStar 📖	CompOp	28 math math: Prod.fst_kstar, kstar_le_of_mul_le_left, kstar_idem, Pi.kstar_apply, mul_kstar_le_self, kstar_mul_le_self, kstar_mul_le_self, one_le_kstar, one_le_kstar, kstar_le_of_mul_le_right, Pi.kstar_def, kstar_mul_kstar, mul_kstar_le_kstar, mul_kstar_le, kstar_one, Prod.snd_kstar, kstar_mono, Prod.kstar_def, le_kstar, pow_le_kstar, mul_kstar_le_self, kstar_eq_self, kstar_mul_le_kstar, kstar_zero, kstar_mul_le, mul_kstar_le_kstar, kstar_mul_le_kstar, kstar_eq_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kstar_mul_le_kstar 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup toIdemSemiring NonUnitalNonAssocSemiring.toMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IdemSemiring.toSemiring KStar.kstar toKStar	—	—
kstar_mul_le_self 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup toIdemSemiring NonUnitalNonAssocSemiring.toMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IdemSemiring.toSemiring	KStar.kstar toKStar	—	—
mul_kstar_le_kstar 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup toIdemSemiring NonUnitalNonAssocSemiring.toMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IdemSemiring.toSemiring KStar.kstar toKStar	—	—
mul_kstar_le_self 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup toIdemSemiring NonUnitalNonAssocSemiring.toMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IdemSemiring.toSemiring	KStar.kstar toKStar	—	—
one_le_kstar 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup toIdemSemiring Semiring.toOne IdemSemiring.toSemiring KStar.kstar toKStar	—	—

LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring	—	add_eq_left_iff_le
add_eq_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring	—	add_eq_right_iff_le

Pi

Definitions

Name	Category	Theorems
instIdemCommSemiringForall 📖	CompOp	—
instIdemSemiring 📖	CompOp	—
instKleeneAlgebraForall 📖	CompOp	2 math math: kstar_apply, kstar_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kstar_apply 📖	mathematical	—	KStar.kstar KleeneAlgebra.toKStar instKleeneAlgebraForall	—	—
kstar_def 📖	mathematical	—	KStar.kstar KleeneAlgebra.toKStar instKleeneAlgebraForall	—	—

Prod

Definitions

Name	Category	Theorems
instIdemCommSemiring 📖	CompOp	—
instIdemSemiring 📖	CompOp	—
instKleeneAlgebra 📖	CompOp	3 math math: fst_kstar, snd_kstar, kstar_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst_kstar 📖	mathematical	—	KStar.kstar KleeneAlgebra.toKStar instKleeneAlgebra	—	—
kstar_def 📖	mathematical	—	KStar.kstar KleeneAlgebra.toKStar instKleeneAlgebra	—	—
snd_kstar 📖	mathematical	—	KStar.kstar KleeneAlgebra.toKStar instKleeneAlgebra	—	—

(root)

Definitions

Name	Category	Theorems
IdemCommSemiring 📖	CompData	—
IdemSemiring 📖	CompData	—
KStar 📖	CompData	—
KleeneAlgebra 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_left_iff_le 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup	—	add_eq_sup
add_eq_right_iff_le 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup	—	add_eq_sup
add_eq_sup 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring SemilatticeSup.toMax IdemSemiring.toSemilatticeSup	—	IdemSemiring.add_eq_sup
add_idem 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring	—	add_eq_sup sup_of_le_left
add_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring	—	add_le_iff
add_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring	—	add_eq_sup
kstar_eq_one 📖	mathematical	—	KStar.kstar KleeneAlgebra.toKStar AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring IdemSemiring.toSemiring KleeneAlgebra.toIdemSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup	—	LE.le.trans_eq le_kstar LE.le.antisymm' one_le_kstar kstar_le_of_mul_le_left le_rfl one_mul
kstar_eq_self 📖	mathematical	—	KStar.kstar KleeneAlgebra.toKStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring KleeneAlgebra.toIdemSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	kstar_mul_kstar LE.le.trans_eq one_le_kstar LE.le.antisymm kstar_le_of_mul_le_left Eq.le le_kstar
kstar_idem 📖	mathematical	—	KStar.kstar KleeneAlgebra.toKStar	—	kstar_eq_self kstar_mul_kstar one_le_kstar
kstar_le_of_mul_le_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring IdemSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	KStar.kstar KleeneAlgebra.toKStar	—	one_mul mul_kstar_le
kstar_le_of_mul_le_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring IdemSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	KStar.kstar KleeneAlgebra.toKStar	—	mul_one kstar_mul_le
kstar_mono 📖	mathematical	—	Monotone PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring KStar.kstar KleeneAlgebra.toKStar	—	kstar_le_of_mul_le_left one_le_kstar kstar_mul_le LE.le.trans le_kstar mul_kstar_le_kstar
kstar_mul_kstar 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring KleeneAlgebra.toIdemSemiring KStar.kstar KleeneAlgebra.toKStar	—	LE.le.antisymm mul_kstar_le le_rfl kstar_mul_le_kstar le_mul_of_one_le_left' IdemSemiring.toMulRightMono one_le_kstar
kstar_mul_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring	KStar.kstar KleeneAlgebra.toKStar	—	le_imp_le_of_le_of_le mul_le_mul_right IdemSemiring.toMulLeftMono le_refl kstar_mul_le_self
kstar_mul_le_kstar 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring KStar.kstar KleeneAlgebra.toKStar	—	KleeneAlgebra.kstar_mul_le_kstar
kstar_mul_le_self 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring	KStar.kstar KleeneAlgebra.toKStar	—	KleeneAlgebra.kstar_mul_le_self
kstar_one 📖	mathematical	—	KStar.kstar KleeneAlgebra.toKStar AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring IdemSemiring.toSemiring KleeneAlgebra.toIdemSemiring	—	kstar_eq_one le_rfl
kstar_zero 📖	mathematical	—	KStar.kstar KleeneAlgebra.toKStar MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring KleeneAlgebra.toIdemSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	kstar_eq_one zero_le IdemSemiring.toCanonicallyOrderedAdd
le_kstar 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring KStar.kstar KleeneAlgebra.toKStar	—	le_trans le_mul_of_one_le_left' IdemSemiring.toMulRightMono one_le_kstar kstar_mul_le_kstar
mul_kstar_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring	KStar.kstar KleeneAlgebra.toKStar	—	le_imp_le_of_le_of_le mul_le_mul_left IdemSemiring.toMulRightMono le_refl mul_kstar_le_self
mul_kstar_le_kstar 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring KStar.kstar KleeneAlgebra.toKStar	—	KleeneAlgebra.mul_kstar_le_kstar
mul_kstar_le_self 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IdemSemiring.toSemiring	KStar.kstar KleeneAlgebra.toKStar	—	KleeneAlgebra.mul_kstar_le_self
natCast_eq_one 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring IdemSemiring.toSemiring AddMonoidWithOne.toOne	—	Nat.le_induction Nat.cast_one Nat.cast_add add_idem
nsmul_eq_self 📖	mathematical	—	AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring IdemSemiring.toSemiring	—	one_nsmul succ_nsmul add_idem
ofNat_eq_one 📖	mathematical	—	AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring IdemSemiring.toSemiring	—	natCast_eq_one Nat.AtLeastTwo.prop
one_le_kstar 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring IdemSemiring.toSemiring KStar.kstar KleeneAlgebra.toKStar	—	KleeneAlgebra.one_le_kstar
pow_le_kstar 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder IdemSemiring.toSemilatticeSup KleeneAlgebra.toIdemSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring KStar.kstar KleeneAlgebra.toKStar	—	Eq.trans_le pow_zero one_le_kstar pow_succ' le_imp_le_of_le_of_le mul_le_mul_right IdemSemiring.toMulLeftMono le_refl mul_kstar_le_kstar

---

← Back to Index