FinitePresentationLocal

📁 Source: Mathlib/RingTheory/Finiteness/FinitePresentationLocal.lean

Statistics

Metric	Count
Definitions	0
Theorems of_span_eq_top_target, of_span_eq_top_target_aux, of_span_eq_top_target_of_isLocalizationAway, pi	4
Total	4

Algebra.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_span_eq_top_target 📖	mathematical	Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.FinitePresentation Localization.Away CommRing.toCommMonoid OreLocalization.instSemiring Ring.toSemiring CommRing.toRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAlgebra	Algebra.FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	—	Ideal.span_eq_top_iff_finite Algebra.FiniteType.of_span_eq_top_target Algebra.FiniteType.of_finitePresentation Algebra.FiniteType.iff_quotient_mvPolynomial'' Finsupp.mem_span_iff_linearCombination map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass map_sum Finset.sum_congr map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Finsupp.linearCombination_apply_of_mem_supported Finset.coe_attach mul_comm sub_self MulZeroClass.zero_mul Ideal.instIsTwoSided_1 Ideal.Quotient.lift_surjective_of_surjective Ideal.eq_top_iff_one eq_of_sub_eq_zero RingHom.instRingHomClass RingHomClass.toAddMonoidHomClass Ideal.Quotient.eq_zero_iff_mem Ideal.subset_span NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Ideal.sum_mem Ideal.mul_mem_right Finset.coe_image Set.image_univ quotient Finset.coe_singleton mvPolynomial self Finite.of_fintype Ideal.Quotient.liftₐ_apply of_span_eq_top_target_aux
of_span_eq_top_target_aux 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike Ideal.span SetLike.coe Finset Finset.instSetLike Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.FinitePresentation Localization.Away CommRing.toCommMonoid SetLike.instMembership OreLocalization.instSemiring Ring.toSemiring CommRing.toRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instAlgebra	Algebra.FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	—	of_surjective RingHom.ker_fg_of_localizationSpan trans OreLocalization.instIsScalarTower IsScalarTower.right IsLocalization.Away.finitePresentation Localization.isLocalization ker_fG_of_surjective IsLocalization.Away.mapₐ_surjective_of_surjective
of_span_eq_top_target_of_isLocalizationAway 📖	mathematical	Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set.range Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsScalarTower Algebra.toSMul IsLocalization.Away Algebra.FinitePresentation	Algebra.FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	—	of_span_eq_top_target equiv OreLocalization.instIsScalarTower IsScalarTower.right Localization.isLocalization
pi 📖	mathematical	Algebra.FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	Algebra.FinitePresentation CommRing.toCommSemiring Pi.semiring CommSemiring.toSemiring Pi.algebra	—	IsLocalization.away_of_isIdempotentElem Pi.single_eq_same mul_one RingHom.ker_evalRingHom RingHom.surjective instRingHomSurjectiveForallEvalRingHom of_span_eq_top_target_of_isLocalizationAway Ideal.span_single_eq_top IsScalarTower.of_algHom

---

← Back to Index