| Metric | Count |
|---|
DefinitionsAddOreLocalization, hvadd, instAdd, instAddActionOfVAddAssocClass, instAddActionOreLocalization, instAddCommMonoid, instAddMonoid, instInhabited, instVAdd, instVAddOfVAddAssocClass, instZero, liftExpand, lift₂Expand, nsmul, numeratorAddUnit, numeratorHom, oreEqv, oreSub, oreSubAddChar', oreSubVAddChar', universalAddHom, vadd, zero, OreLocalization, hsmul, instCommMonoid, instInhabited, instMonoid, instMul, instMulActionOfIsScalarTower, instMulActionOreLocalization, instOne, instSMul, instSMulOfIsScalarTower, instZero, liftExpand, lift₂Expand, npow, numeratorHom, numeratorUnit, one, oreDiv, oreDivMulChar', oreDivSMulChar', oreEqv, smul, universalMulHom, zero, «term_-ₒ_», «term_/ₒ_», «term__[_⁻¹_]» | 51 |
Theoremsadd_assoc, add_cancel, add_cancel', add_neg, add_sub_zero, add_vadd, add_zero, eq_of_num_factor_eq, expand, expand', ind, instIsCentralVAdd, instVAddAssocClass, instVAddAssocClass_1, instVAddCommClass, instVAddCommClass_1, liftExpand_of, lift₂Expand_of, numeratorHom_apply, numerator_isAddUnit, oreSub_add_char, oreSub_add_oreSub, oreSub_add_oreSub_comm, oreSub_eq_iff, oreSub_vadd_char, oreSub_vadd_oreSub, oreSub_zero_vadd, sub_eq_zero, sub_eq_zero', universalAddHom_apply, universalAddHom_commutes, universalAddHom_unique, vadd_cancel, vadd_cancel', vadd_oreSub, vadd_oreSub_zero, vadd_sub_zero, vadd_zero_oreSub_zero_vadd, vadd_zero_vadd, zero_add, zero_def, zero_sub_add, zero_sub_vadd, zero_vadd, div_eq_one, div_eq_one', eq_of_num_factor_eq, expand, expand', ind, instIsCentralScalar, instIsScalarTower, instIsScalarTower_1, instSMulCommClass, instSMulCommClass_1, liftExpand_of, lift₂Expand_of, mul_assoc, mul_cancel, mul_cancel', mul_div_one, mul_inv, mul_one, mul_smul, numeratorHom_apply, numerator_isUnit, one_def, one_div_mul, one_div_smul, one_mul, one_smul, oreDiv_eq_iff, oreDiv_mul_char, oreDiv_mul_oreDiv, oreDiv_mul_oreDiv_comm, oreDiv_one_smul, oreDiv_smul_char, oreDiv_smul_oreDiv, smul_cancel, smul_cancel', smul_div_one, smul_one_oreDiv_one_smul, smul_one_smul, smul_oreDiv, smul_oreDiv_one, universalMulHom_apply, universalMulHom_commutes, universalMulHom_unique, zero_def | 89 |
| Total | 140 |
| Name | Category | Theorems |
|---|
hvadd 📖 | CompOp | — |
instAdd 📖 | CompOp | 21 mathmath: oreSub_add_oreSub, add_cancel, add_sub_zero, oreSub_add_char, AddLocalization.addEquivOfQuotient_mk', add_zero, AddLocalization.addEquivOfQuotient_apply, add_vadd, AddLocalization.addEquivOfQuotient_mk, AddLocalization.addEquivOfQuotient_symm_mk', AddLocalization.mk_add, zero_add, AddLocalization.addEquivOfQuotient_symm_mk, add_assoc, add_cancel', AddLocalization.addEquivOfQuotient_addMonoidOf, AddLocalization.addEquivOfQuotient_symm_addMonoidOf, oreSub_add_oreSub_comm, zero_sub_add, add_neg, AddSubmonoid.LocalizationMap.instIsCancelAddLocalization
|
instAddActionOfVAddAssocClass 📖 | CompOp | — |
instAddActionOreLocalization 📖 | CompOp | — |
instAddCommMonoid 📖 | CompOp | 14 mathmath: AddLocalization.isOrderedAddCancelMonoid, AddLocalization.liftOn_mk', AddLocalization.mk_zero_eq_addMonoidOf_mk, AddLocalization.addEquivOfQuotient_mk', AddLocalization.mk_eq_addMonoidOf_mk', AddLocalization.addEquivOfQuotient_apply, AddLocalization.addEquivOfQuotient_symm_mk', AddLocalization.mk_sum, AddLocalization.liftOn₂_mk', AddLocalization.Away.mk_eq_addMonoidOf_mk', Algebra.GrothendieckAddGroup.lift_apply, AddLocalization.addEquivOfQuotient_addMonoidOf, AddLocalization.addEquivOfQuotient_symm_addMonoidOf, AddLocalization.mk_eq_addMonoidOf_mk'_apply
|
instAddMonoid 📖 | CompOp | 14 mathmath: Algebra.GrothendieckAddGroup.instFG, numerator_isAddUnit, AddLocalization.fg, numeratorHom_surjective_of_finite, numeratorHom_apply, Algebra.GrothendieckAddGroup.of_injective, AddLocalization.mkHom_apply, AddLocalization.mkHom_surjective, AddLocalization.instIsAddTorsionFree, universalAddHom_commutes, Algebra.GrothendieckAddGroup.lift_apply, universalAddHom_apply, AddLocalization.mk_nsmul, Algebra.GrothendieckAddGroup.lift_symm_apply
|
instInhabited 📖 | CompOp | — |
instVAdd 📖 | CompOp | 12 mathmath: instVAddCommClass_1, instVAddAssocClass_1, vadd_zero_oreSub_zero_vadd, vadd_cancel', add_vadd, oreSub_vadd_char, zero_vadd, oreSub_zero_vadd, zero_sub_vadd, vadd_sub_zero, vadd_cancel, oreSub_vadd_oreSub
|
instVAddOfVAddAssocClass 📖 | CompOp | 10 mathmath: vadd_oreSub_zero, instVAddAssocClass, instVAddCommClass_1, vadd_oreSub, instVAddAssocClass_1, vadd_zero_oreSub_zero_vadd, instIsCentralVAdd, oreSub_zero_vadd, vadd_zero_vadd, instVAddCommClass
|
instZero 📖 | CompOp | 10 mathmath: sub_eq_zero', sub_eq_zero, AddLocalization.mk_self, AddLocalization.mk_self_mk, add_zero, zero_vadd, AddLocalization.mk_zero, zero_add, add_neg, zero_def
|
liftExpand 📖 | CompOp | 1 mathmath: liftExpand_of
|
lift₂Expand 📖 | CompOp | 1 mathmath: lift₂Expand_of
|
nsmul 📖 | CompOp | — |
numeratorAddUnit 📖 | CompOp | — |
numeratorHom 📖 | CompOp | 4 mathmath: numerator_isAddUnit, numeratorHom_surjective_of_finite, numeratorHom_apply, universalAddHom_commutes
|
oreEqv 📖 | CompOp | 1 mathmath: AddLocalization.r_iff_oreEqv_r
|
oreSub 📖 | CompOp | 31 mathmath: oreSub_add_oreSub, sub_eq_zero', vadd_oreSub_zero, sub_eq_zero, oreSub_eq_iff, oreSub_zero_surjective_of_finite_left, add_cancel, vadd_oreSub, oreSub_zero_surjective_of_finite_right, add_sub_zero, oreSub_add_char, vadd_zero_oreSub_zero_vadd, vadd_cancel', numeratorHom_apply, expand, oreSub_vadd_char, lift₂Expand_of, add_cancel', oreSub_zero_vadd, universalAddHom_apply, zero_sub_vadd, eq_of_num_factor_eq, oreSub_add_oreSub_comm, vadd_sub_zero, vadd_cancel, zero_sub_add, expand', add_neg, liftExpand_of, zero_def, oreSub_vadd_oreSub
|
oreSubAddChar' 📖 | CompOp | — |
oreSubVAddChar' 📖 | CompOp | — |
universalAddHom 📖 | CompOp | 3 mathmath: universalAddHom_commutes, universalAddHom_apply, universalAddHom_unique
|
vadd 📖 | CompOp | — |
zero 📖 | CompOp | — |
| Name | Category | Theorems |
|---|
hsmul 📖 | CompOp | — |
instCommMonoid 📖 | CompOp | 16 mathmath: Localization.Away.mk_eq_monoidOf_mk', Localization.mk_eq_monoidOf_mk', Localization.mulEquivOfQuotient_symm_monoidOf, Localization.isOrderedCancelMonoid, HomogeneousLocalization.val_awayMap, Localization.liftOn₂_mk', Localization.mk_one_eq_monoidOf_mk, Localization.mk_eq_monoidOf_mk'_apply, Localization.mulEquivOfQuotient_mk', Localization.monoidOf_eq_algebraMap, Localization.mk_prod, Localization.mulEquivOfQuotient_monoidOf, Localization.mulEquivOfQuotient_apply, Algebra.GrothendieckGroup.lift_apply, Localization.liftOn_mk', Localization.mulEquivOfQuotient_symm_mk'
|
instInhabited 📖 | CompOp | — |
instMonoid 📖 | CompOp | 26 mathmath: numeratorHom_surjective_of_finite, Algebra.GrothendieckGroup.instFG, Localization.instIsMulTorsionFree, instIsLocalHomAtPrimeRingHomAlgebraMap, HomogeneousLocalization.val_pow, numeratorHom_inj, Algebra.GrothendieckGroup.lift_symm_apply, Localization.mkHom_surjective, ModuleCat.instIsScalarTowerLocalizationCarrierLocalizedModule, Localization.fg, IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower_1, numeratorHom_apply, universalMulHom_apply, instIsReducedLocalization, ClassGroup.equivPic_symm_apply, HomogeneousLocalization.isUnit_iff_isUnit_val, Localization.mk_pow, Localization.mkHom_apply, numerator_isUnit, IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower, universalMulHom_commutes, Localization.isLocalHom_localRingHom, Algebra.GrothendieckGroup.lift_apply, ClassGroup.equivPic_apply, Algebra.GrothendieckGroup.of_injective, universalHom_commutes
|
instMul 📖 | CompOp | 39 mathmath: left_distrib, mul_smul, WittVector.IsocrystalHom.frob_equivariant, Localization.mulEquivOfQuotient_symm_monoidOf, mul_zero, oreDiv_mul_oreDiv, mul_div_one, mul_assoc, WittVector.IsocrystalEquiv.frob_equivariant, Localization.mulEquivOfQuotient_mk, Localization.instNoZeroDivisors, mul_cancel, mul_one, Localization.mulEquivOfQuotient_mk', HomogeneousLocalization.val_mul, right_distrib, WittVector.inv_pair₂, WittVector.exists_frobenius_solution_fractionRing, one_div_mul, Localization.mulEquivOfQuotient_symm_mk, WittVector.inv_pair₁, mul_cancel', zero_mul, mul_inv, oreDiv_mul_char, WittVector.StandardOneDimIsocrystal.frobenius_apply, Localization.mulEquivOfQuotient_monoidOf, Localization.mulEquivOfQuotient_apply, mul_inv_cancel, oreDiv_mul_oreDiv_comm, WittVector.exists_frobenius_solution_fractionRing_aux, Localization.mk_mul, one_mul, Submonoid.LocalizationMap.instIsCancelMulLocalization, RatFunc.toFractionRingRingEquiv_symm_eq, RatFunc.toFractionRingRingEquiv_apply, Localization.mulEquivOfQuotient_symm_mk', RatFunc.mul_def, RatFunc.ofFractionRing_mul
|
instMulActionOfIsScalarTower 📖 | CompOp | — |
instMulActionOreLocalization 📖 | CompOp | — |
instOne 📖 | CompOp | 15 mathmath: HomogeneousLocalization.val_one, one_smul, LocalizedModule.equivTensorProduct_symm_apply_tmul_one, div_eq_one, RatFunc.ofFractionRing_one, mul_one, RatFunc.one_def, Localization.mk_self, mul_inv, div_eq_one', Localization.mk_one, mul_inv_cancel, one_def, one_mul, Localization.mk_self_mk
|
instSMul 📖 | CompOp | 20 mathmath: mul_smul, smul_cancel', zero_smul, one_smul, smul_cancel, IsLocalization.instIsScalarTowerLocalizationAtPrime, smul_one_oreDiv_one_smul, instIsScalarTower_1, WittVector.StandardOneDimIsocrystal.frobenius_apply, oreDiv_smul_oreDiv, smul_add, instSMulCommClass_1, LocalizedModule.mk_smul_mk, smul_div_one, LocalizedModule.smul_eq_iff_of_mem, one_div_smul, oreDiv_smul_char, smul_zero, add_smul, oreDiv_one_smul
|
instSMulOfIsScalarTower 📖 | CompOp | 52 mathmath: instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl, FractionRing.instIsScalarTower, LocalizedModule.restrictScalars_map_eq, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, RatFunc.mk_smul, instIsScalarTowerAtPrimeFractionRing_1, LocalizedModule.lift'_smul, smul_oreDiv_one, HomogeneousLocalization.val_smul, LocalizedModule.equivTensorProduct_symm_apply_tmul, Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, IsLocalization.instIsScalarTowerLocalizationAtPrime, RatFunc.smul_eq_C_mul, instSMulCommClass, ModuleCat.instIsScalarTowerLocalizationCarrierLocalizedModule, HomogeneousLocalization.instIsScalarTowerSubtypeMemOfNatLocalization, RatFunc.smul_eq_C_smul, RatFunc.instIsScalarTowerOfIsDomainOfPolynomial, LocalizedModule.smul'_mk, RatFunc.div_smul, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, RatFunc.faithfulSMul, instIsCentralScalar, RatFunc.instIsScalarTowerPolynomial, smul_one_oreDiv_one_smul, instIsScalarTower_1, RatFunc.instIsScalarTowerOfPolynomial, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, smul_oreDiv, IsLocalization.instIsScalarTowerAtPrimeFractionRing, Localization.AtPrime.instIsScalarTower, LocalizedModule.instIsScalarTower, Localization.smul_mk, HomogeneousLocalization.Away.eventually_smul_mem, Localization.instFaithfulSMulAtPrimeOfNoZeroDivisors, instSMulCommClass_1, HomogeneousLocalization.den_smul_val, LocalizedModule.smul_eq_iff_of_mem, RatFunc.isScalarTower_liftAlgebra, FractionRing.isScalarTower_liftAlgebra, instIsScalarTower, instIsScalarTowerLocalizationAlgebraMapSubmonoid, FractionRing.instFaithfulSMul, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1, AlgebraicGeometry.structureSheafInType.smul_apply, smul_one_smul, oreDiv_one_smul, IsLocalizedModule.fromLocalizedModule'_smul
|
instZero 📖 | CompOp | 28 mathmath: Localization.liftOn_zero, mul_zero, add_zero, neg_add_cancel, HomogeneousLocalization.val_zero, zero_smul, RatFunc.ofFractionRing_zero, DivisibleHull.instIsStrictOrderedModuleNNRat, Localization.instNoZeroDivisors, zero_add, zero_def, Localization.mk_list_sum, RatFunc.zero_def, zero_mul, zero_oreDiv, instIsReducedLocalization, LocalizedModule.map_exact, RatFunc.mk_zero, zero_oreDiv', Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, DivisibleHull.instIsStrictOrderedModuleRat, DivisibleHull.mk_zero, DivisibleHull.zero_qsmul, inv_zero, LocalizedModule.zero_mk, smul_zero, Localization.mk_zero, inv_def
|
liftExpand 📖 | CompOp | 1 mathmath: liftExpand_of
|
lift₂Expand 📖 | CompOp | 1 mathmath: lift₂Expand_of
|
npow 📖 | CompOp | — |
numeratorHom 📖 | CompOp | 6 mathmath: numeratorHom_surjective_of_finite, numeratorHom_inj, numeratorHom_apply, numerator_isUnit, universalMulHom_commutes, universalHom_commutes
|
numeratorUnit 📖 | CompOp | — |
one 📖 | CompOp | — |
oreDiv 📖 | CompOp | 42 mathmath: oreDiv_add_char, oreDiv_eq_iff, oreDiv_one_surjective_of_finite_right, universalHom_apply, smul_cancel', smul_oreDiv_one, oreDiv_mul_oreDiv, neg_def, eq_of_num_factor_eq, mul_div_one, smul_cancel, oreDiv_add_char', div_eq_one, expand', expand, numeratorRingHom_apply, oreDiv_add_oreDiv, mul_cancel, one_div_mul, smul_one_oreDiv_one_smul, zero_def, mul_cancel', numeratorHom_apply, universalMulHom_apply, zero_oreDiv, mul_inv, liftExpand_of, div_eq_one', oreDiv_mul_char, smul_oreDiv, lift₂Expand_of, oreDiv_smul_oreDiv, oreDiv_mul_oreDiv_comm, zero_oreDiv', one_def, oreDiv_one_surjective_of_finite_left, smul_div_one, add_oreDiv, one_div_smul, oreDiv_smul_char, oreDiv_one_smul, inv_def
|
oreDivMulChar' 📖 | CompOp | — |
oreDivSMulChar' 📖 | CompOp | — |
oreEqv 📖 | CompOp | 2 mathmath: Localization.r_iff_oreEqv_r, LocalizedModule.oreEqv_eq_r
|
smul 📖 | CompOp | — |
universalMulHom 📖 | CompOp | 3 mathmath: universalMulHom_unique, universalMulHom_apply, universalMulHom_commutes
|
zero 📖 | CompOp | — |
«term_-ₒ_» 📖 | CompOp | — |
«term_/ₒ_» 📖 | CompOp | — |
«term__[_⁻¹_]» 📖 | CompOp | — |