Basic

📁 Source: Mathlib/Data/Int/Order/Basic.lean

Statistics

Metric	Count
Definitions instLinearOrder	1
Theorems eq_zero_or_eq_zero_of_mul_eq_zero, elim, le_of_ofNat_le_ofNat, elim, lt_of_ofNat_lt_ofNat, mul_neg_iff, mul_nonneg_iff, mul_nonneg_of_nonneg_or_nonpos, mul_nonpos_iff, mul_pos_iff, nonneg_or_nonpos_of_mul_nonneg, ofNat_le_ofNat_of_le, ofNat_lt_ofNat_of_lt	13
Total	14

Int

Definitions

Name	Category	Theorems
instLinearOrder 📖	CompOp	391 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, ComplexShape.embeddingUpIntDownInt_f, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', ValuationSubring.integralClosure_algebraMap_injective, NumberField.FinitePlace.mk_apply, floor_int, Padic.withValUniformEquiv_norm_le_one_iff, Rat.padicValuation_cast, HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc, CategoryTheory.InjectiveResolution.ι'_f_zero, zpow_right_anti₀, IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff_mem_primeCompl, WeierstrassCurve.HasAdditiveReduction.badReduction, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, HomologicalComplex₂.shiftFunctor₂XXIso_refl, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₃, NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, CochainComplex.instIsStrictlyLEObjHomologicalComplexIntUpSingle, Set.unit_eq, Padic.instCompatibleWithZeroMultiplicativeIntMulValuation, NumberField.FinitePlace.norm_def', DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, FunctionField.inftyValuation.X_inv, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, padicValuation_lt_one_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, NumberField.FinitePlace.embedding_apply, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, CochainComplex.mappingCone.homologySequenceδ_triangleh, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, LaurentSeries.valuation_single_zpow, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc, IsDedekindDomain.HeightOneSpectrum.intValuation_le_one, WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral, NumberField.HeightOneSpectrum.rankOne_hom'_def, CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdIntCoreE₂Cohomological, CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_apply, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, Nat.ceil_int, AbsoluteValue.abs_isEuclidean, IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntValuation, padicValuation_eq_one_iff, RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc, CochainComplex.shiftShortComplexFunctorIso_add'_hom_app, CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso, CochainComplex.HomComplex.Cochain.toSingleMk_v, CochainComplex.IsKInjective.rightOrthogonal, CochainComplex.IsKInjective.Qh_map_bijective, HomotopyCategory.instIsHomologicalIntUpHomologyFunctor, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem, Padic.addValuation.apply, IsDedekindDomain.HeightOneSpectrum.intValuation_singleton, FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, Rat.padicValuation_self, RatFunc.coe_X, CochainComplex.instIsStrictlyGEObjHomologicalComplexIntUpSingle, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', HomologicalComplex₂.ι_totalShift₁Iso_inv_f, RatFunc.coe_coe, NumberField.FinitePlace.norm_embedding_eq, Polynomial.valuation_of_mk, ComplexShape.eulerCharSignsUpInt_χ, WeierstrassCurve.hasGoodReduction_iff, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq, DerivedCategory.shiftMap_homologyFunctor_map_Q_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, LaurentSeries.inducing_coe, CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjective, LaurentSeries.continuous_coe, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, RatFunc.adicValuation_not_isEquiv_infty_valuation, CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKInjective, CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk, HomotopyCategory.instAdditiveIntUpShiftFunctor, WeierstrassCurve.hasMultiplicativeReduction_iff, Padic.norm_eq_zpow_log_mulValuation, PowerSeries.intValuation_eq_of_coe, instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences, FunctionField.instIsTrivialOnWithZeroMultiplicativeIntRatFuncInftyValuation, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, NumberField.FinitePlace.norm_embedding, ceil_int, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, LaurentSeries.val_le_one_iff_eq_coe, NumberField.HeightOneSpectrum.adicAbv_def, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer, IsDiscreteValuationRing.isRankOneDiscrete, CochainComplex.homologyFunctor_shift, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, Valued.tendsto_zero_pow_of_le_exp_neg_one, FunctionField.valuedFqtInfty.def, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, DerivedCategory.shiftMap_homologyFunctor_map_Qh_assoc, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, HomotopyCategory.Pretriangulated.complete_distinguished_triangle_morphism, IsDedekindDomain.HeightOneSpectrum.valuation_def, HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₂, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, FunctionField.InftyValuation.map_add_le_max', IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_1, Nat.floor_int, LaurentSeries.exists_ratFunc_val_lt, HomotopyCategory.mappingCone_triangleh_distinguished, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, CochainComplex.HomComplex.Cochain.fromSingleMk_v, Padic.mulValuation_toFun, IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff, RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one, WeierstrassCurve.HasGoodReduction.goodReduction, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd, HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂, IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max', Padic.comap_mulValuation_eq_padicValuation, NumberField.FinitePlace.norm_lt_one_iff_mem, Rat.valuation_le_one_iff_den, strictMono_int_of_lt_succ, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, RatFunc.valuation_surjective, CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_symm_apply, instQFactorsThroughHomotopyIntUp, LaurentSeries.exists_Polynomial_intValuation_lt, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor, fract_int, DerivedCategory.instAdditiveHomotopyCategoryIntUpQh, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, ValuationSubring.instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, HomologicalComplex₂.shiftFunctor₁XXIso_refl, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le, IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, RatFunc.valuation_eq_LaurentSeries_valuation, CochainComplex.mappingCone.map_inr, CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, PadicInt.coe_adicCompletionIntegersEquiv_apply, HomotopyCategory.instLinearIntUpShiftFunctor, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂, HomotopyCategory.Pretriangulated.distinguished_cocone_triangle, HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, LaurentSeries.coe_X_compare, NumberField.HeightOneSpectrum.embedding_mul_absNorm, HomotopyCategory.instLinearIntUpSingleFunctor, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, ComplexShape.eulerCharSignsDownInt_χ, HomotopyCategory.instAdditiveIntUpSingleFunctor, monotone_int_of_le_succ, RatFunc.algebraMap_apply_div, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, HomotopyCategory.Pretriangulated.contractible_distinguished, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₂, ComplexShape.instIsRelIffIntEmbeddingDownIntUpInt, padicValuation_self, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.continuous_coe', NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply, CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, NumberField.FinitePlace.norm_def_int, WeierstrassCurve.hasAdditiveReduction_iff, CochainComplex.IsKProjective.Qh_map_bijective, WeierstrassCurve.HasAdditiveReduction.additiveReduction, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, ValuationSubring.isIntegral_of_mem_ringOfIntegers', DerivedCategory.instEssSurjHomotopyCategoryIntUpQh, CategoryTheory.ProjectiveResolution.π'_f_zero, antitone_int_of_succ_le, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd, HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic, RatFunc.valuation_isEquiv_infty_or_adic, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f, IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring, HomotopyCategory.instIsTriangulatedIntUp, DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, HomologicalComplex₂.D₁_totalShift₁XIso_hom, IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt, HomologicalComplex₂.D₂_totalShift₁XIso_hom, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, LaurentSeries.valuation_LaurentSeries_equal_extension, RatFunc.v_def, Rat.padicValuation_eq_zero_iff, LaurentSeries.LaurentSeries_coe, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff, LaurentSeries.powerSeries_ext_subring, Set.unit_valuation_eq_one, NumberField.HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers, ValuationSubring.isIntegral_of_mem_ringOfIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic, FunctionField.inftyValuation.X_zpow, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, LaurentSeries.powerSeriesRingEquiv_coe_apply, CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt, HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.intValuation_def, DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, FunctionField.inftyValuation.X, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_deg, HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W, CochainComplex.IsKProjective.leftOrthogonal, FunctionField.inftyValuedFqt.def, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, RatFunc.valuation_isEquiv_adic_of_not_isEquiv_infty, strictAnti_int_of_succ_lt, CochainComplex.isKProjective_iff_leftOrthogonal, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, LaurentSeries.instLaurentSeriesComplete, IsDedekindDomain.HeightOneSpectrum.valuation_surjective, HomotopyCategory.mem_subcategoryAcyclic_iff, exists_strictMono, Padic.withValUniformEquiv_cast_apply, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁, LaurentSeries.valuation_surjective, LaurentSeries.valuation_coe_ratFunc, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, Padic.coe_withValRingEquiv, Padic.comap_mulValuation_eq_int_padicValuation, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, NumberField.FinitePlace.norm_eq_one_iff_notMem, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, HomotopyCategory.homologyFunctor_shiftMap_assoc, HomologicalComplex₂.totalShift₂Iso_hom_naturality, HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, ComplexShape.σ_def, DerivedCategory.shiftMap_homologyFunctor_map_Q, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂, LaurentSeries.tendsto_valuation, HomotopyCategory.spectralObjectMappingCone_ω₁, CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_symm_apply, LaurentSeries.coe_range_dense, CochainComplex.shiftEval_hom_app, PowerSeries.intValuation_X, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f, Padic.coe_withValRingEquiv_symm, RatFunc.valuation_isEquiv_inftyValuation_of_one_lt_valuation_X, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, exists_strictAnti, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, LaurentSeries.comparePkg_eq_extension, HomotopyCategory.homologyShiftIso_hom_app, DerivedCategory.Qh_obj_singleFunctors_obj, RatFunc.single_zpow, HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc, LaurentSeries.valuation_def, IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntIntValuation, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle', FunctionField.inftyValuation.C, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, Rat.HeightOneSpectrum.valuation_equiv_padicValuation, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₁, LaurentSeries.uniformContinuous_coeff, zpow_right_mono₀, Padic.norm_rat_le_one_iff_padicValuation_le_one, Set.integer_valuation_le_one, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, Rat.surjective_padicValuation, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle, HomologicalComplex₂.totalShift₁Iso_hom_naturality, HomotopyCategory.quotient_obj_singleFunctors_obj, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f, IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer, zpow_right_strictMono₀, CochainComplex.shiftEval_inv_app, DerivedCategory.shiftMap_homologyFunctor_map_Qh, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁, RootPairing.RootPositiveForm.rootLength_le_of_pairingIn_eq, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₀, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, Ico_filter_modEq_eq, Set.integer_eq, Ioc_filter_modEq_eq, ComplexShape.ε_up_ℤ, HomotopyCategory.homologyFunctor_shiftMap, CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app, ComplexShape.embeddingDownIntUpInt_f, HomotopyCategory.Pretriangulated.invRotate_distinguished_triangle', padicValuation_le_one, HomologicalComplex₂.D₁_totalShift₂XIso_hom, DerivedCategory.instLinearHomotopyCategoryIntUpQh, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, NumberField.FinitePlace.norm_embedding', HomotopyCategory.Pretriangulated.isomorphic_distinguished, CochainComplex.mappingConeCompTriangleh_comm₁, HomologicalComplex₂.D₂_totalShift₂XIso_hom, NumberField.FinitePlace.norm_le_one, WeierstrassCurve.HasMultiplicativeReduction.badReduction, CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_apply, LaurentSeries.mem_integers_of_powerSeries, RootPairing.RootPositiveForm.rootLength_lt_of_pairingIn_notMem, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj, Valuation.IsRankOneDiscrete.generator_eq_neg_exp_one_of_surjective, CochainComplex.isKInjective_iff_rightOrthogonal, ValuationSubring.algebraMap_injective, CochainComplex.ShiftSequence.shiftIso_inv_app, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, RatFunc.single_inv, Valued.exists_pow_lt_of_le_exp_neg_one, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₁, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq, ComplexShape.instIsRelIffIntEmbeddingUpIntDownInt, DerivedCategory.isIso_Qh_map_iff, CochainComplex.liftCycles_shift_homologyπ_assoc, FunctionField.inftyValuation_apply, NumberField.FinitePlace.norm_embedding_int, LaurentSeries.exists_ratFunc_eq_v, HomotopyCategory.mappingConeCompTriangleh_distinguished, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, Padic.isDenseInducing_cast_withVal, LaurentSeries.uniformContinuous_withVal_equiv, HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, IsDedekindDomain.HeightOneSpectrum.intValuation_apply, LaurentSeries.valuation_X_pow, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem, padicValuation_eq_zero_iff, HomotopyCategory.Pretriangulated.shift_distinguished_triangle, NumberField.FinitePlace.norm_def, WeierstrassCurve.HasMultiplicativeReduction.multiplicativeReduction, CochainComplex.liftCycles_shift_homologyπ, Rat.padicValuation_le_one_iff, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, zpow_right_strictAnti₀, CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, Polynomial.valuation_X_eq_neg_one, CochainComplex.ShiftSequence.shiftIso_hom_app, HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, CochainComplex.mappingCone.map_δ, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic, DerivedCategory.instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_or_eq_zero_of_mul_eq_zero 📖	—	—	—	—	—
le_of_ofNat_le_ofNat 📖	—	—	—	—	—
lt_of_ofNat_lt_ofNat 📖	—	—	—	—	—
mul_neg_iff 📖	—	—	—	—	not_iff_not not_lt mul_nonneg_iff
mul_nonneg_iff 📖	—	—	—	—	nonneg_or_nonpos_of_mul_nonneg mul_nonneg_of_nonneg_or_nonpos
mul_nonneg_of_nonneg_or_nonpos 📖	—	—	—	—	—
mul_nonpos_iff 📖	—	—	—	—	not_iff_not not_le mul_pos_iff
mul_pos_iff 📖	—	—	—	—	mul_nonneg_iff
nonneg_or_nonpos_of_mul_nonneg 📖	—	—	—	—	—
ofNat_le_ofNat_of_le 📖	—	—	—	—	—
ofNat_lt_ofNat_of_lt 📖	—	—	—	—	—

Int.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elim 📖	—	—	—	—	—

Int.lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elim 📖	—	—	—	—	—

---

← Back to Index