Documentation Verification Report

Proper

📁 Source: Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean

Statistics

Metric	Count
Definitions	0
Theorems `instIsProperToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`, `instIsSeparated`, `instLocallyOfFiniteTypeToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`, `instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`, `instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`, `isSeparated`, `lift_awayMapₐ_awayMapₐ_surjective`, `valuativeCriterion_existence`, `valuativeCriterion_existence_aux`	9
Total	9

AlgebraicGeometry.Proj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsProperToSpecZeroOfFiniteTypeSubtypeMemOfNatNat` 📖	mathematical	—	`AlgebraicGeometry.IsProper` `AlgebraicGeometry.Proj` `AlgebraicGeometry.Spec` `CommRingCat.of` `SetLike.instMembership` `SetLike.GradeZero.instCommRing` `Nat.instAddCommMonoid` `GradedRing.toGradedMonoid` `AddCommMonoid.toAddMonoid` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toSpecZero`	—	`AddSubgroupClass.toAddSubmonoidClass` `GradedRing.toGradedMonoid` `isSeparated` `instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemOfNatNat` `instLocallyOfFiniteTypeToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`
`instIsSeparated` 📖	mathematical	—	`AlgebraicGeometry.Scheme.IsSeparated` `AlgebraicGeometry.Proj`	—	`AddSubgroupClass.toAddSubmonoidClass` `GradedRing.toGradedMonoid` `AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `AlgebraicGeometry.IsSeparated.hasAffineProperty` `AlgebraicGeometry.isAffine_Spec` `isSeparated`
`instLocallyOfFiniteTypeToSpecZeroOfFiniteTypeSubtypeMemOfNatNat` 📖	mathematical	—	`AlgebraicGeometry.LocallyOfFiniteType` `AlgebraicGeometry.Proj` `AlgebraicGeometry.Spec` `CommRingCat.of` `SetLike.instMembership` `SetLike.GradeZero.instCommRing` `Nat.instAddCommMonoid` `GradedRing.toGradedMonoid` `AddCommMonoid.toAddMonoid` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toSpecZero`	—	`AddSubgroupClass.toAddSubmonoidClass` `GradedRing.toGradedMonoid` `GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero` `AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource` `AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType` `iSup_basicOpen_eq_top'` `Subtype.range_coe_subtype` `Ne.bot_lt` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Category.assoc` `awayι.eq_1` `awayι_toSpecZero` `AlgebraicGeometry.HasRingHomProperty.Spec_iff` `HomogeneousLocalization.Away.finiteType`
`instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat` 📖	mathematical	—	`AlgebraicGeometry.QuasiCompact` `AlgebraicGeometry.Proj` `AlgebraicGeometry.Spec` `CommRingCat.of` `SetLike.instMembership` `SetLike.GradeZero.instCommRing` `Nat.instAddCommMonoid` `GradedRing.toGradedMonoid` `AddCommMonoid.toAddMonoid` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toSpecZero`	—	`AddSubgroupClass.toAddSubmonoidClass` `GradedRing.toGradedMonoid` `AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `AlgebraicGeometry.isAffine_Spec` `GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero` `Ne.bot_lt` `instIsOpenImmersionAwayι` `opensRange_awayι` `isCompact_range` `AlgebraicGeometry.Scheme.compactSpace_of_isAffine` `AlgebraicGeometry.Scheme.Hom.continuous` `iSup_basicOpen_eq_top'` `Subtype.range_coe_subtype` `isCompact_univ_iff` `isOpen_iUnion` `TopologicalSpace.Opens.is_open'` `isCompact_iUnion` `Finite.of_fintype`
`instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemOfNatNat` 📖	mathematical	—	`AlgebraicGeometry.UniversallyClosed` `AlgebraicGeometry.Proj` `AlgebraicGeometry.Spec` `CommRingCat.of` `SetLike.instMembership` `SetLike.GradeZero.instCommRing` `Nat.instAddCommMonoid` `GradedRing.toGradedMonoid` `AddCommMonoid.toAddMonoid` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toSpecZero`	—	`AddSubgroupClass.toAddSubmonoidClass` `GradedRing.toGradedMonoid` `AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion` `valuativeCriterion_existence` `instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`
`isSeparated` 📖	mathematical	—	`AlgebraicGeometry.IsSeparated` `AlgebraicGeometry.Proj` `AlgebraicGeometry.Spec` `CommRingCat.of` `SetLike.instMembership` `SetLike.GradeZero.instCommRing` `Nat.instAddCommMonoid` `GradedRing.toGradedMonoid` `AddCommMonoid.toAddMonoid` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toSpecZero`	—	`AddSubgroupClass.toAddSubmonoidClass` `GradedRing.toGradedMonoid` `AlgebraicGeometry.IsZariskiLocalAtTarget.of_openCover` `AlgebraicGeometry.IsClosedImmersion.isZariskiLocalAtTarget` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `CategoryTheory.Category.comp_id` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `AlgebraicGeometry.IsClosedImmersion.respectsIso` `CategoryTheory.Iso.isIso_inv` `awayι_toSpecZero` `CategoryTheory.MorphismProperty.cancel_right_of_respectsIso` `CategoryTheory.Iso.isIso_hom` `Algebra.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `mul_comm` `Commute.all` `lift_awayMapₐ_awayMapₐ_surjective` `CategoryTheory.cancel_mono` `AlgebraicGeometry.IsOpenImmersion.mono` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst` `AlgebraicGeometry.pullbackSpecIso_inv_fst` `AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right` `instIsOpenImmersionAwayι` `pullbackAwayιIso_inv_fst` `CommRingCat.hom_ext` `RingHom.ext` `DFunLike.congr_fun` `Algebra.TensorProduct.lift_comp_includeLeft` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd` `AlgebraicGeometry.pullbackSpecIso_inv_snd` `pullbackAwayιIso_inv_snd` `TensorProduct.isScalarTower_left` `Algebra.TensorProduct.lift_comp_includeRight` `AlgebraicGeometry.IsClosedImmersion.spec_of_surjective`
`lift_awayMapₐ_awayMapₐ_surjective` 📖	mathematical	`SetLike.instMembership` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`TensorProduct` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `SetLike.GradeZero.instCommSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `GradedRing.toGradedMonoid` `CommSemiring.toSemiring` `HomogeneousLocalization.Away` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.toModule` `HomogeneousLocalization.instAlgebraSubtypeMemOfNat` `DFunLike.coe` `AlgHom` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `Algebra.id` `IsScalarTower.left` `SetLike.GradeZero.instMonoid` `DistribMulAction.toMulAction` `Module.toDistribMulAction` `SetLike.GradeZero.instSemiring` `AlgHom.funLike` `Algebra.TensorProduct.lift` `HomogeneousLocalization.awayMapₐ` `mul_comm` `NonUnitalNonAssocCommSemiring.toCommMagma` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring` `Commute.all`	—	`AddSubgroupClass.toAddSubmonoidClass` `GradedRing.toGradedMonoid` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `mul_comm` `Commute.all` `HomogeneousLocalization.mk_surjective` `HomogeneousLocalization.subsingleton` `DirectSum.degree_eq_of_mem_mem` `SetLike.pow_mem_graded` `SetLike.mul_mem_graded` `SetLike.GradedMonoid.toGradedMul` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.nsmul_congr` `Mathlib.Tactic.Ring.smul_nat` `HomogeneousLocalization.val_injective` `Submonoid.mem_powers_iff` `HomogeneousLocalization.NumDenSameDeg.den_mem` `HomogeneousLocalization.val_mul` `Localization.mk_mul` `Localization.mk_eq_mk_iff` `Localization.r_iff_exists` `one_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw`
`valuativeCriterion_existence` 📖	mathematical	—	`AlgebraicGeometry.ValuativeCriterion.Existence` `AlgebraicGeometry.Proj` `AlgebraicGeometry.Spec` `CommRingCat.of` `SetLike.instMembership` `SetLike.GradeZero.instCommRing` `Nat.instAddCommMonoid` `GradedRing.toGradedMonoid` `AddCommMonoid.toAddMonoid` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `toSpecZero`	—	`AddSubgroupClass.toAddSubmonoidClass` `GradedRing.toGradedMonoid` `AlgebraicGeometry.ValuativeCommSq.commSq` `GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero` `ValuationRing.isLocalRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ValuationRing.toPreValuationRing` `instIsDomain` `ValuationRing.of_field` `TopologicalSpace.Opens.mem_iSup` `iSup_basicOpen_eq_top'` `Subtype.range_coe_subtype` `Ne.bot_lt` `instIsOpenImmersionAwayι` `opensRange_awayι` `Unique.instSubsingleton` `AlgebraicGeometry.Spec.map_injective` `AlgebraicGeometry.Spec.map_comp` `AlgebraicGeometry.Spec.map_preimage` `CategoryTheory.CommSq.w` `awayι_toSpecZero` `AlgebraicGeometry.IsOpenImmersion.lift_fac_assoc` `mul_comm` `valuativeCriterion_existence_aux` `Finite.of_fintype` `IsFractionRing.injective` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `RingHom.ext` `RingEquiv.apply_symm_apply` `AlgebraicGeometry.Spec.map_comp_assoc` `CommRingCat.ofHom_hom` `CommRingCat.ofHom_comp` `SetLike.mul_mem_graded` `SetLike.GradedMonoid.toGradedMul` `add_comm` `LT.lt.trans_le` `CategoryTheory.Category.assoc` `SpecMap_awayMap_awayι` `awayι.congr_simp` `AlgebraicGeometry.IsOpenImmersion.lift_fac` `CommRingCat.hom_ext` `DFunLike.congr_fun` `HomogeneousLocalization.awayMap_fromZeroRingHom` `RingHom.comp_apply`
`valuativeCriterion_existence_aux` 📖	mathematical	`Algebra.adjoin` `SetLike.instMembership` `SetLike.GradeZero.instCommSemiring` `CommRing.toCommSemiring` `Nat.instAddMonoid` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `GradedRing.toGradedMonoid` `CommSemiring.toSemiring` `SetLike.GradeZero.instAlgebraSubtypeMemOfNat` `Set.range` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `RingHom.comp` `Semiring.toNonAssocSemiring` `SetLike.GradeZero.instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `algebraMap` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `HomogeneousLocalization.Away` `HomogeneousLocalization.homogeneousLocalizationCommRing` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `HomogeneousLocalization.fromZeroRingHom`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `HomogeneousLocalization.awayMap` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `Subring.instPartialOrder` `RingHom.range` `mul_comm` `NonUnitalNonAssocCommSemiring.toCommMagma` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring`	—	`AddSubgroupClass.toAddSubmonoidClass` `GradedRing.toGradedMonoid` `nonempty_fintype` `mul_comm` `Finset.max'_mem` `Finset.le_max'` `zero_lt_iff` `le_zero_iff` `HomogeneousLocalization.val_injective` `HomogeneousLocalization.val_one` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `isReduced_of_noZeroDivisors` `GroupWithZero.noZeroDivisors` `ValuationRing.instNontrivialValueGroup` `map_one` `MonoidHomClass.toOneHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `NeZero.one` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `HomogeneousLocalization.Away.isLocalization_mul` `LT.lt.ne'` `isUnit_iff_ne_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `zero_pow` `Nat.instNontrivial` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsLocalization.Away.lift_eq` `IsLocalization.Away.lift_comp` `RingHom.mem_range` `ValuationRing.mem_integer_iff` `Valuation.mem_integer_iff` `SetLike.prod_pow_mem_graded` `Eq.ge` `HomogeneousLocalization.Away.span_mk_prod_pow_eq_top` `Submodule.mem_top` `Submodule.span_induction` `Finset.sum_congr` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `SetLike.mul_mem_graded` `SetLike.GradedMonoid.toGradedMul` `SetLike.pow_mem_graded` `map_div₀` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `LinearOrderedCommMonoidWithZero.toMulPosStrictMono` `LT.lt.trans_eq` `pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `Valuation.pos_iff` `IsUnit.ne_zero` `Valuation.map_pow` `one_mul` `pow_le_pow_iff_left₀` `MulPosStrictMono.toMulPosMono` `zero_le'` `LT.lt.ne` `mul_pos` `Finset.prod_pos` `Nat.instZeroLEOneClass` `Finset.prod_congr` `MonoidHomClass.toMulHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_mul` `map_prod` `Submonoid.instSubmonoidClass` `Localization.mk_pow` `Localization.mk_prod` `Localization.mk_mul` `Localization.mk_eq_mk_iff` `Localization.r_iff_exists` `SubmonoidClass.coe_finset_prod` `Finset.prod_erase_mul` `Finset.mem_univ` `mul_assoc` `Finset.prod_pow_eq_pow_sum` `mul_pow` `mul_left_comm` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `Finset.prod_le_prod` `PosMulStrictMono.toPosMulMono` `pow_le_pow_left₀` `pow_add` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `pow_mul` `mul_right_comm` `eq_div_iff` `pow_ne_zero` `IsDomain.to_noZeroDivisors` `instIsDomain` `RingHom.comp_apply` `HomogeneousLocalization.val_mul` `HomogeneousLocalization.val_pow` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `LE.le.trans` `Valuation.map_add` `sup_le_iff` `Algebra.smul_def` `mul_le_one'` `RingHom.algebraMap_toAlgebra` `HomogeneousLocalization.awayMap_fromZeroRingHom`

---

← Back to Index