Quotient

📁 Source: Mathlib/RingTheory/Trace/Quotient.lean

Statistics

Metric	Count
Definitions	0
Theorems trace_quotient_eq_of_isDedekindDomain, trace_quotient_mk, trace_quotient_eq_trace_localization_quotient	3
Total	3

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trace_quotient_eq_of_isDedekindDomain 📖	mathematical	—	DFunLike.coe LinearMap HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.commRing RingHom.id Semiring.toNonAssocSemiring Ideal.map RingHom RingHom.instFunLike algebraMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Ideal.Quotient.algebraQuotientMapQuotient Semiring.toModule LinearMap.instFunLike trace Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 intTrace IsDedekindDomain.toIsDomain IsDedekindDomainDvr.isIntegrallyClosed IsDedekindDomain.isDedekindDomainDvr	—	Ideal.IsMaximal.isPrime' Submonoid.map_le_of_le_comap LE.le.trans Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors IsDedekindDomain.toIsDomain nonZeroDivisors_le_comap_nonZeroDivisors_of_injective RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial IsDedekindDomain.isPrincipalIdealRing Localization.AtPrime.isLocalRing Localization.AtPrime.isDedekindDomain IsLocalization.isDomain_of_local_atPrime IsDedekindDomainDvr.is_dvr_at_nonzero_prime IsDedekindDomain.isDedekindDomainDvr IsDiscreteValuationRing.toIsPrincipalIdealRing RingEquiv.injective Localization.isLocalization Ideal.instIsTwoSided_1 IsDedekindDomainDvr.isIntegrallyClosed trace_quotient_eq_trace_localization_quotient OreLocalization.instIsScalarTower IsScalarTower.right IsScalarTower.of_algebraMap_eq' RingHom.algebraMap_toAlgebra IsLocalization.map_comp IsScalarTower.algebraMap_eq Ideal.Quotient.isScalarTower RingHom.comp_apply Ideal.Quotient.algebraMap_eq Module.free_of_finite_type_torsion_free' Module.Finite.of_isLocalization Module.isTorsionFree_iff_algebraMap_injective IsLocalization.isDomain_of_le_nonZeroDivisors RingHom.injective_iff_ker_eq_bot RingHom.ker_eq_bot_iff_eq_zero Module.Free.instFaithfulSMulOfNontrivial instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain RingEquiv.apply_symm_apply isIntegrallyClosed_of_isLocalization intTrace_eq_trace intTrace_eq_of_isLocalization IsScalarTower.algebraMap_apply
trace_quotient_mk 📖	mathematical	—	DFunLike.coe LinearMap HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 IsLocalRing.maximalIdeal Ideal.Quotient.commRing RingHom.id Semiring.toNonAssocSemiring Ideal.map RingHom RingHom.instFunLike algebraMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule Ideal.Quotient.algebraQuotientMapQuotient Semiring.toModule LinearMap.instFunLike trace Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1	—	Ideal.instIsTwoSided_1 trace_eq_matrix_trace AddMonoidHom.map_trace RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype to_smulCommClass IsScalarTower.right LinearMap.toMatrix_apply IsLocalRing.basisQuotient_apply NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass IsLocalRing.basisQuotient_repr

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trace_quotient_eq_trace_localization_quotient 📖	mathematical	—	DFunLike.coe LinearMap HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.commRing RingHom.id Semiring.toNonAssocSemiring Ideal.map RingHom RingHom.instFunLike algebraMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Ideal.Quotient.algebraQuotientMapQuotient Semiring.toModule LinearMap.instFunLike Algebra.trace Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingEquiv IsLocalRing.maximalIdeal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm IsLocalization.AtPrime.equivQuotMaximalIdeal Ideal.Quotient.semiring Ideal.instAlgebraQuotient	—	Ideal.IsMaximal.isPrime' IsScalarTower.right IsScalarTower.of_algebraMap_eq' IsScalarTower.algebraMap_eq Ideal.Quotient.isScalarTower RingHom.comp_assoc Ideal.Quotient.tower_quotient_map_quotient Ideal.instIsTwoSided_1 Algebra.trace_eq_of_equiv_equiv Ideal.Quotient.ringHom_ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.ext IsScalarTower.algebraMap_apply

---

← Back to Index