Documentation Verification Report

Basic

📁 Source: Mathlib/RingTheory/OreLocalization/Basic.lean

Statistics

Metric	Count
Definitions `instAdd`, `instAddCommGroup`, `instAddCommMonoidOreLocalization`, `instAddGroupOreLocalization`, `instAddMonoid`, `instCommMonoidWithZero`, `instDistribMulAction`, `instDistribMulActionOfIsScalarTower`, `instMonoidWithZero`, `instNegOreLocalization`, `neg`, `oreDivAddChar'`, `zsmul`	13
Theorems `add_assoc`, `add_comm`, `add_oreDiv`, `add_zero`, `neg_add_cancel`, `neg_def`, `nontrivial_iff`, `oreDiv_add_char`, `oreDiv_add_char'`, `oreDiv_add_oreDiv`, `smul_add`, `smul_zero`, `subsingleton_iff`, `zero_add`, `zero_oreDiv`, `zero_oreDiv'`	16
Total	29

OreLocalization

Definitions

Name	Category	Theorems
`instAdd` 📖	CompOp	33 math math: `left_distrib`, `oreDiv_add_char`, `WittVector.IsocrystalHom.frob_equivariant`, `LocalizedModule.mk_add_mk`, `DivisibleHull.mk_add_mk_left`, `add_zero`, `neg_add_cancel`, `oreDiv_add_char'`, `RatFunc.ofFractionRing_add`, `WittVector.IsocrystalEquiv.frob_equivariant`, `oreDiv_add_oreDiv`, `zero_add`, `HomogeneousLocalization.val_add`, `right_distrib`, `WittVector.inv_pair₂`, `WittVector.inv_pair₁`, `Localization.mk_list_sum`, `IsLocalizedModule.fromLocalizedModule'_add`, `AlgebraicGeometry.structureSheafInType.add_apply`, `add_assoc`, `WittVector.StandardOneDimIsocrystal.frobenius_apply`, `DivisibleHull.mk_add_mk`, `Localization.add_mk`, `smul_add`, `DivisibleHull.coe_add`, `add_oreDiv`, `RatFunc.add_def`, `add_comm`, `RatFunc.toFractionRingRingEquiv_symm_eq`, `RatFunc.toFractionRingRingEquiv_apply`, `LocalizedModule.lift'_add`, `add_smul`, `Localization.add_mk_self`
`instAddCommGroup` 📖	CompOp	6 math math: `DivisibleHull.archimedeanClassMk_mk_eq`, `Module.freeLocus_localization`, `instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient`, `DivisibleHull.archimedeanClassOrderIso_apply`, `DivisibleHull.archimedeanClassOrderIso_symm_apply`, `instFiniteDimensionalFractionRingOfFinite`
`instAddCommMonoidOreLocalization` 📖	CompOp	93 math math: `IsLocalizedModule.iso_symm_apply'`, `Module.Finite.instLocalizationLocalizedModule`, `LocalizedModule.restrictScalars_map_eq`, `Module.Flat.localizedModule`, `nsmul_eq_nsmul`, `Module.FinitePresentation.exists_notMem_bijective`, `IsLocalizedModule.iso_symm_apply`, `Module.basicOpen_subset_freeLocus_iff`, `IsLocalizedModule.iso_apply_mk`, `LocalizedModule.divBy_apply`, `Module.associatedPrimes.mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes`, `LocalizedModule.divBy_mul_by`, `LocalizedModule.map_surjective`, `IsLocalizedModule.map_surjective_iff_localizedModuleMap_surjective`, `LocalizedModule.mem_ker_mkLinearMap_iff`, `IsLocalizedModule.fromLocalizedModule.bij`, `LocalizedModule.equivTensorProduct_symm_apply_tmul_one`, `LocalizedModule.equivTensorProduct_apply_mk`, `LocalizedModule.map_injective`, `LocalizedModule.equivTensorProduct_symm_apply_tmul`, `Module.FinitePresentation.linearEquivMap_symm_apply`, `IsLocalizedModule.iso_symm_comp`, `IsLocalizedModule.fromLocalizedModule.inj`, `Algebra.WeaklyQuasiFiniteAt.finite_locoalization`, `DivisibleHull.instIsStrictOrderedModuleNNRat`, `Localization.mk_sum`, `LocalizedModule.coe_map_eq`, `zsmul_eq_zsmul`, `LocalizedModule.subsingleton_iff_ker_eq_top`, `Module.FinitePresentation.exists_free_localizedModule_powers`, `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂`, `IsLocalizedModule.fromLocalizedModule_mk`, `Module.rankAtStalk_eq_finrank_tensorProduct`, `Module.FinitePresentation.linearEquivMap_apply`, `Ideal.relNorm_algebraMap'`, `Localization.finite_of_primesOver_eq_singleton`, `instFinitePresentationLocalizationLocalizedModule`, `IsLocalizedModule.lift_comp_iso`, `DivisibleHull.instIsOrderedCancelAddMonoid`, `localizedModuleIsLocalizedModule`, `Ideal.relNorm_algebraMap`, `instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient`, `LocalizedModule.lift_comp`, `instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1`, `DivisibleHull.qsmul_def`, `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq`, `instFlatAtPrime`, `DivisibleHull.qsmul_of_nonneg`, `Module.FinitePresentation.linearEquivMapExtendScalars_apply`, `IsLocalizedModule.iso_symm_apply_aux`, `Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain`, `ClassGroup.equivPic_symm_apply`, `LocalizedModule.lift_mk`, `Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule`, `instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl`, `instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl`, `IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective`, `LocalizedModule.mul_by_divBy`, `LocalizedModule.map_exact`, `instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors`, `LocalizedModule.map_id`, `Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes`, `AlgebraicGeometry.StructureSheaf.Localizations.comapFun_mk`, `Algebra.IsAlgebraic.rank_fractionRing`, `instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl`, `LocalizedModule.lift_mk_one`, `Module.Invertible.instLocalizationLocalizedModule`, `IsLocalizedModule.mk_eq_mk'`, `IsLocalizedModule.map_injective_iff_localizedModuleMap_injective`, `DivisibleHull.qsmul_of_nonpos`, `Localization.mk_multiset_sum`, `exists_bijective_map_powers`, `IsLocalizedModule.iso_localizedModule_eq_refl`, `Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial`, `LocalizedModule.map_mk`, `instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2`, `IsLocalizedModule.fromLocalizedModule.surj`, `Localization.flat`, `MvRatFunc.rank_eq_max_lift`, `Module.mem_freeLocus`, `ClassGroup.equivPic_apply`, `IsLocalizedModule.map_iso_commute`, `Ideal.absNorm_algebraMap`, `IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain`, `instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation`, `IsLocalizedModule.map_LocalizedModules`, `Algebra.IsAlgebraic.rank_fractionRing_polynomial`, `IsLocalizedModule.lift_iso`, `LocalizedModule.mkLinearMap_apply`, `Module.FinitePresentation.exists_basis_localizedModule_powers`, `DivisibleHull.nnqsmul_mk`, `IsLocalizedModule.iso_mk_one`, `Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply`
`instAddGroupOreLocalization` 📖	CompOp	8 math math: `HomogeneousLocalization.val_zsmul`, `HomogeneousLocalization.val_sub`, `zsmul_eq_zsmul`, `DivisibleHull.qsmul_def`, `RatFunc.ofFractionRing_sub`, `DivisibleHull.zsmul_mk`, `RatFunc.sub_def`, `Localization.sub_mk`
`instAddMonoid` 📖	CompOp	13 math math: `HomogeneousLocalization.val_nsmul`, `nsmul_eq_nsmul`, `DivisibleHull.instIsStrictOrderedModuleNNRat`, `Localization.mkAddMonoidHom_apply`, `DivisibleHull.coeAddMonoidHom_apply`, `DivisibleHull.qsmul_def`, `DivisibleHull.qsmul_of_nonneg`, `DivisibleHull.coeOrderAddMonoidHom_apply`, `DivisibleHull.nsmul_mk`, `Surreal.dyadicMap_apply`, `DivisibleHull.qsmul_of_nonpos`, `Surreal.dyadicMap_apply_pow`, `DivisibleHull.nnqsmul_mk`
`instCommMonoidWithZero` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	—
`instDistribMulActionOfIsScalarTower` 📖	CompOp	—
`instMonoidWithZero` 📖	CompOp	—
`instNegOreLocalization` 📖	CompOp	9 math math: `neg_add_cancel`, `neg_def`, `LocalizedModule.mk_neg`, `RatFunc.ofFractionRing_neg`, `HomogeneousLocalization.val_neg`, `RatFunc.neg_def`, `DivisibleHull.neg_mk`, `DivisibleHull.qsmul_of_nonpos`, `Localization.neg_mk`
`neg` 📖	CompOp	—
`oreDivAddChar'` 📖	CompOp	—
`zsmul` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_assoc` 📖	mathematical	—	`OreLocalization` `DistribMulAction.toMulAction` `instAdd`	—	`ind` `smul_add` `add_assoc` `expand`
`add_comm` 📖	mathematical	—	`OreLocalization` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `instAdd`	—	`ind` `oreDiv_add_char'` `add_comm`
`add_oreDiv` 📖	mathematical	—	`OreLocalization` `DistribMulAction.toMulAction` `instAdd` `oreDiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`oreDiv_add_char` `one_mul` `one_smul`
`add_zero` 📖	mathematical	—	`OreLocalization` `DistribMulAction.toMulAction` `instAdd` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`ind` `zero_oreDiv` `add_oreDiv` `add_zero`
`neg_add_cancel` 📖	mathematical	—	`OreLocalization` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instAdd` `instNegOreLocalization` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ind` `neg_def` `add_oreDiv` `neg_add_cancel` `zero_oreDiv`
`neg_def` 📖	mathematical	—	`OreLocalization` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instNegOreLocalization` `oreDiv` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`nontrivial_iff` 📖	mathematical	—	`Nontrivial` `OreLocalization` `MonoidWithZero.toMonoid` `MulActionWithZero.toMulAction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZero.toMulActionWithZero` `Submonoid` `MulZeroOneClass.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike`	—	`not_subsingleton_iff_nontrivial` `subsingleton_iff`
`oreDiv_add_char` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`OreLocalization` `DistribMulAction.toMulAction` `instAdd` `oreDiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Submonoid.mul`	—	`oreDiv_add_char'`
`oreDiv_add_char'` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`OreLocalization` `DistribMulAction.toMulAction` `instAdd` `oreDiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`oreDiv_add_oreDiv` 📖	mathematical	—	`OreLocalization` `DistribMulAction.toMulAction` `instAdd` `oreDiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `oreDenom` `oreNum` `Submonoid.mul`	—	—
`smul_add` 📖	mathematical	—	`OreLocalization` `Monoid.toMulAction` `DistribMulAction.toMulAction` `instSMul` `instAdd`	—	`ind` `expand'` `SubmonoidClass.toMulMemClass` `Submonoid.instSubmonoidClass` `SetLike.coe_mem` `expand` `oreDiv_smul_oreDiv` `smul_add` `add_oreDiv`
`smul_zero` 📖	mathematical	—	`OreLocalization` `Monoid.toMulAction` `DistribMulAction.toMulAction` `instSMul` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`ind` `zero_def` `smul_div_one` `smul_zero` `zero_oreDiv`
`subsingleton_iff` 📖	mathematical	—	`OreLocalization` `MonoidWithZero.toMonoid` `MulActionWithZero.toMulAction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZero.toMulActionWithZero` `Submonoid` `MulZeroOneClass.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike`	—	`subsingleton_iff_zero_eq_one` `one_def` `zero_def` `oreDiv_eq_iff` `MulZeroClass.mul_zero` `mul_one`
`zero_add` 📖	mathematical	—	`OreLocalization` `DistribMulAction.toMulAction` `instAdd` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`ind` `zero_oreDiv` `add_oreDiv` `zero_add`
`zero_oreDiv` 📖	mathematical	—	`oreDiv` `DistribMulAction.toMulAction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `OreLocalization` `instZero`	—	`zero_def` `oreDiv_eq_iff` `smul_zero` `mul_one` `one_mul`
`zero_oreDiv'` 📖	mathematical	—	`oreDiv` `MonoidWithZero.toMonoid` `MulActionWithZero.toMulAction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZero.toMulActionWithZero` `OreLocalization` `instZero`	—	`zero_def` `oreDiv_eq_iff` `MulZeroClass.mul_zero` `mul_one` `one_mul`

---

← Back to Index