Prod

📁 Source: Mathlib/Algebra/Ring/Prod.lean

Statistics

Metric	Count
Definitions fst, prod, prodMap, snd, instCommRing, instCommSemiring, instDistrib, instNonAssocRing, instNonAssocSemiring, instNonUnitalCommRing, instNonUnitalCommSemiring, instNonUnitalNonAssocRing, instNonUnitalNonAssocSemiring, instNonUnitalRing, instNonUnitalSemiring, instRing, instSemiring, prodComm, prodProdProdComm, prodZeroRing, zeroRingProd, fst, prod, prodMap, snd	25
Theorems coe_fst, coe_prodMap, coe_snd, fst_comp_prod, prodMap_def, prod_apply, prod_comp_prodMap, prod_unique, snd_comp_prod, coe_prodComm, coe_prodComm_symm, fst_comp_coe_prodComm, prodProdProdComm_apply, prodProdProdComm_symm, prodProdProdComm_toAddEquiv, prodProdProdComm_toEquiv, prodProdProdComm_toMulEquiv, prodZeroRing_apply, prodZeroRing_symm_apply, snd_comp_coe_prodComm, zeroRingProd_apply, zeroRingProd_symm_apply, coe_fst, coe_prodMap, coe_snd, fst_comp_prod, instRingHomSurjectiveProdFst, instRingHomSurjectiveProdSnd, prodMap_def, prod_apply, prod_comp_prodMap, prod_unique, snd_comp_prod, false_of_nontrivial_of_product_domain	34
Total	59

NonUnitalRingHom

Definitions

Name	Category	Theorems
fst 📖	CompOp	8 math math: fst_comp_prod, NonUnitalSubring.prod_top, prodMap_def, NonUnitalSubsemiring.range_fst, NonUnitalSubsemiring.prod_top, prod_unique, NonUnitalSubring.range_fst, coe_fst
prod 📖	CompOp	6 math math: snd_comp_prod, fst_comp_prod, prod_comp_prodMap, prodMap_def, prod_unique, prod_apply
prodMap 📖	CompOp	3 math math: coe_prodMap, prod_comp_prodMap, prodMap_def
snd 📖	CompOp	8 math math: snd_comp_prod, NonUnitalSubsemiring.top_prod, coe_snd, prodMap_def, NonUnitalSubring.range_snd, NonUnitalSubring.top_prod, NonUnitalSubsemiring.range_snd, prod_unique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_fst 📖	mathematical	—	DFunLike.coe NonUnitalRingHom Prod.instNonUnitalNonAssocSemiring instFunLike fst	—	—
coe_prodMap 📖	mathematical	—	DFunLike.coe NonUnitalRingHom Prod.instNonUnitalNonAssocSemiring instFunLike prodMap	—	—
coe_snd 📖	mathematical	—	DFunLike.coe NonUnitalRingHom Prod.instNonUnitalNonAssocSemiring instFunLike snd	—	—
fst_comp_prod 📖	mathematical	—	comp Prod.instNonUnitalNonAssocSemiring fst prod	—	ext
prodMap_def 📖	mathematical	—	prodMap prod Prod.instNonUnitalNonAssocSemiring comp fst snd	—	—
prod_apply 📖	mathematical	—	DFunLike.coe NonUnitalRingHom Prod.instNonUnitalNonAssocSemiring instFunLike prod	—	—
prod_comp_prodMap 📖	mathematical	—	comp Prod.instNonUnitalNonAssocSemiring prodMap prod	—	—
prod_unique 📖	mathematical	—	prod comp Prod.instNonUnitalNonAssocSemiring fst snd	—	ext
snd_comp_prod 📖	mathematical	—	comp Prod.instNonUnitalNonAssocSemiring snd prod	—	ext

Prod

Definitions

Name	Category	Theorems
instCommRing 📖	CompOp	16 math math: AlgebraicGeometry.coprodSpec_apply, AlgebraicGeometry.coprodSpec_inr, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, AlgebraicGeometry.isIso_stalkMap_coprodSpec, Algebra.trace_prod, AlgebraicGeometry.coprodSpec_coprodMk, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, AlgebraicGeometry.coprodSpec_inr_assoc, AlgebraicGeometry.coprodSpec_inl_assoc, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, AlgebraicGeometry.coprodSpec_inl, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, Algebra.trace_prod_apply, AlgebraicGeometry.instIsIsoSchemeCoprodSpec, CommRingCat.prodFan_pt
instCommSemiring 📖	CompOp	13 math math: AlgebraicGeometry.coprodSpec_apply, PrimeSpectrum.isClosedEmbedding_comap_snd, PrimeSpectrum.primeSpectrumProd_symm_inl, PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal, PrimeSpectrum.isClosedEmbedding_comap_fst, IsLocalization.away_snd, PrimeSpectrum.primeSpectrumProd_symm_inr, AlgebraicGeometry.coprodSpec_coprodMk, PrimeSpectrum.range_comap_snd, PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal, IsLocalization.away_fst, PrimeSpectrum.range_comap_fst, instPerfectRingProd
instDistrib 📖	CompOp	—
instNonAssocRing 📖	CompOp	—
instNonAssocSemiring 📖	CompOp	70 math math: Subring.range_snd, NumberField.mixedEmbedding.convexBodyLT'_mem, RingHom.snd_comp_prod, Ideal.map_fst_prod, DoubleCentralizer.nnnorm_def', NumberField.mixedEmbedding.norm_eq_norm, NumberField.mixedEmbedding.mem_idealLattice, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, RingHom.prod_unique, RingEquiv.snd_comp_coe_prodComm, NumberField.mixedEmbedding.convexBodyLT_mem, Subsemiring.coe_prod, DoubleCentralizer.norm_def', Subsemiring.prod_top, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, Subsemiring.prod_mono_right, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, RingHom.prod_comp_prodMap, NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq, NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet, Subsemiring.top_prod_top, Ideal.fst_comp_quotientMulEquivQuotientProd, RingHom.coe_fst, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.logMap_eq_logEmbedding, IsLocalRing.exists_surjective_of_not_isLocalRing, RingHom.prodMap_def, RingHom.fst_comp_prod, Ideal.ideal_prod_eq, Ideal.map_snd_prod, Subsemiring.range_fst, NumberField.mixedEmbedding.mixedEmbedding_apply_isReal, RingHom.prod_bijective_of_isIdempotentElem, NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding, PrimeSpectrum.range_comap_snd, Ideal.snd_comp_quotientMulEquivQuotientProd, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, Subsemiring.range_snd, NumberField.mixedEmbedding.unitSMul_smul, RingHom.coe_snd, NumberField.mixedEmbedding.normAtPlace_apply, NumberField.mixedEmbedding_injective, NumberField.mixedEmbedding.latticeBasis_apply, NumberField.mixedEmbedding.latticeBasis_repr_apply, Subsemiring.prod_mono_left, Subsemiring.prod_bot_sup_bot_prod, RingHom.prod_apply, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, Subring.range_fst, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, Subsemiring.top_prod, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, NumberField.mixedEmbedding.mixedEmbedding_apply_isComplex, Ideal.fst_comp_quotientInfEquivQuotientProd, Ideal.map_prodComm_prod, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet, PrimeSpectrum.range_comap_fst, Ideal.snd_comp_quotientInfEquivQuotientProd, RingHom.coe_prodMap, NumberField.mixedEmbedding.commMap_canonical_eq_mixed, RingEquiv.fst_comp_coe_prodComm, NumberField.mixedEmbedding.norm_unit, Subsemiring.mem_prod, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, NumberField.mixedEmbedding.convexBodySum_mem, LinearMap.prodMapRingHom_apply, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, DoubleCentralizer.toProdMulOppositeHom_apply, Subsemiring.prod_mono
instNonUnitalCommRing 📖	CompOp	—
instNonUnitalCommSemiring 📖	CompOp	—
instNonUnitalNonAssocRing 📖	CompOp	9 math math: NonUnitalSubring.prod_top, NonUnitalSubring.top_prod, NonUnitalSubring.prod_mono_left, NonUnitalSubring.top_prod_top, NonUnitalSubring.prod_mono, NonUnitalSubring.mem_prod, instIsTopologicalRingProd, NonUnitalSubring.prod_mono_right, NonUnitalSubring.coe_prod
instNonUnitalNonAssocSemiring 📖	CompOp	65 math math: NonUnitalStarSubalgebra.prod_toNonUnitalSubalgebra, NonUnitalStarAlgHom.inl_apply, instIsTopologicalSemiringProd, NonUnitalRingHom.snd_comp_prod, NonUnitalAlgHom.fst_toFun, NonUnitalSubsemiring.top_prod, NonUnitalRingHom.fst_comp_prod, NonUnitalSubring.prod_top, NonUnitalStarAlgHom.prodEquiv_symm_apply, NonUnitalSubalgebra.prod_inf_prod, NonUnitalRingHom.coe_prodMap, NonUnitalSubalgebra.prod_top, NonUnitalAlgHom.prod_apply, NonUnitalSubsemiring.prod_mono, NonUnitalRingHom.coe_snd, NonUnitalStarAlgHom.prod_fst_snd, NonUnitalAlgHom.prod_fst_snd, NonUnitalAlgHom.prodEquiv_apply, NonUnitalRingHom.prod_comp_prodMap, NonUnitalAlgHom.prodEquiv_symm_apply, NonUnitalStarAlgHom.prod_apply, NonUnitalRingHom.prodMap_def, NonUnitalAlgHom.coe_inr, NonUnitalSubring.range_snd, NonUnitalStarAlgHom.inr_apply, NonUnitalAlgHom.coe_prod, NonUnitalSubring.top_prod, NonUnitalStarAlgHom.snd_apply, NonUnitalAlgHom.inl_apply, NonUnitalStarAlgHom.prodEquiv_apply, NonUnitalAlgHom.snd_prod, NonUnitalSubsemiring.prod_mono_left, NonUnitalStarSubalgebra.prod_mono, NonUnitalStarAlgHom.fst_apply, NonUnitalStarSubalgebra.prod_inf_prod, NonUnitalSubsemiring.range_fst, NonUnitalAlgHom.fst_prod, NonUnitalAlgHom.snd_apply, NonUnitalSubalgebra.coe_prod, NonUnitalAlgHom.coe_inl, NonUnitalSubsemiring.top_prod_top, NonUnitalAlgHom.prod_toFun, NonUnitalStarAlgHom.fst_prod, NonUnitalSubsemiring.coe_prod, NonUnitalStarAlgHom.coe_prod, NonUnitalStarSubalgebra.coe_prod, NonUnitalStarAlgHom.snd_prod, NonUnitalAlgHom.inr_apply, NonUnitalSubsemiring.prod_top, NonUnitalSubsemiring.prod_mono_right, NonUnitalStarAlgHom.coe_inr, NonUnitalSubsemiring.mem_prod, NonUnitalStarAlgHom.coe_inl, NonUnitalStarSubalgebra.prod_top, NonUnitalAlgHom.fst_apply, NonUnitalSubalgebra.prod_toSubmodule, NonUnitalSubsemiring.range_snd, NonUnitalStarSubalgebra.mem_prod, NonUnitalSubalgebra.mem_prod, NonUnitalRingHom.prod_unique, NonUnitalSubalgebra.prod_mono, NonUnitalSubring.range_fst, NonUnitalRingHom.coe_fst, NonUnitalAlgHom.snd_toFun, NonUnitalRingHom.prod_apply
instNonUnitalRing 📖	CompOp	5 math math: CFC.sqrt_map_prod, cfcₙ_map_prod, CFC.nnrpow_eq_nnrpow_prod, quasispectrum_eq, CFC.nnrpow_map_prod
instNonUnitalSemiring 📖	CompOp	4 math math: instStarOrderedRing, NonUnitalStarSubalgebra.prod_inf_prod, isQuasiregular_prod_iff, NonUnitalStarSubalgebra.prod_top
instRing 📖	CompOp	29 math math: IsIntegral.pair, Subring.top_prod, cfc_map_prod, NonarchimedeanRing.instProd, Algebra.IsIntegral.prod, spectrum_eq, Int.card_box, Subring.mem_prod, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, Subring.prod_mono_left, Subring.top_prod_top, IsIntegral.pair_iff, CFC.rpow_map_prod, instIsSemisimpleRingProd, Subring.prod_bot_sup_bot_prod, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, Int.existsUnique_mem_box, Subring.prod_top, fst_exp, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, Int.mem_box, card_box_succ, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, Subring.coe_prod, snd_exp, Subring.prod_mono, CFC.rpow_eq_rpow_prod, Subring.prod_mono_right
instSemiring 📖	CompOp	96 math math: Ideal.isPrime_ideal_prod_top, instIsOrderedRingProd, ContinuousAlgHom.coe_fst, Algebra.TensorProduct.prodRight_tmul_fst, Ideal.span_prod, Ideal.map_fst_prod, Unitization.splitMul_apply, Algebra.TensorProduct.prodRight_symm_tmul, StarAlgHom.prodEquiv_apply, AlgHom.snd_prod, AlgEquiv.prodQuotientOfIsIdempotentElem_apply, Ideal.ideal_prod_prime, StarAlgHom.snd_apply, StarAlgHom.coe_prod, Subalgebra.prod_mono, Subalgebra.prod_inf_prod, Unitization.nnnorm_def, AlgEquiv.prodCongr_apply, Ideal.prod_bot_bot, Ideal.isPrime_ideal_prod_top', Ideal.prod_mono_left, Polynomial.aeval_prod_apply, Polynomial.aeval_prod, AlgEquiv.sumArrowEquivProdArrow_symm_apply_inr, AlgHom.prodEquiv_symm_apply, Unitization.splitMul_injective_of_clm_mul_injective, Subalgebra.FG.prod, AlgHom.coe_prod, RingHom.instRingHomSurjectiveProdSnd, StarAlgHom.snd_prod, AlgHom.fst_apply, ContinuousAlgHom.coe_prod, isPrincipalIdealRing_prod_iff, Ideal.idealProdEquiv_symm_apply, DoubleCentralizer.algebraMap_toProd, Ideal.ideal_prod_eq, Ideal.map_snd_prod, Ideal.prod_mono_right, AlgHom.snd_apply, Algebra.adjoin_inl_union_inr_eq_prod, Ideal.prod_mono, Ideal.prod_eq_top_iff, StarAlgHom.prod_fst_snd, LinearMap.prodMapAlgHom_apply_apply, PrimeSpectrum.range_comap_snd, Unitization.norm_def, ContinuousAlgHom.coe_prodMap, IsLocalRing.not_isLocalRing_of_prod_of_nontrivial, algebraMap_apply, ContinuousAlgHom.coe_fst', Algebra.adjoin_prod_le, ContinuousAlgHom.prodEquiv_apply, Algebra.FiniteType.prod, AlgEquiv.prodUnique_apply, AlgEquiv.prodQuotientOfIsIdempotentElem_apply_snd, AlgHom.prod_fst_snd, StarAlgHom.prod_apply, instIsPrincipalIdealRingProd, RingHom.instRingHomSurjectiveProdFst, ContinuousAlgHom.coe_prodMap', AlgEquiv.prodQuotientOfIsIdempotentElem_apply_fst, Ideal.prod_eq_bot_iff, StarAlgHom.prodEquiv_symm_apply, Subalgebra.prod_top, AlgHom.prodEquiv_apply, Ideal.coe_prod, ContinuousAlgHom.fst_comp_prod, Ideal.prod_top_top, Unitization.norm_splitMul_snd_sq, Algebra.TensorProduct.prodRight_tmul, Algebra.TensorProduct.prodRight_tmul_snd, Unitization.splitMul_injective, ContinuousAlgHom.fst_prod_snd, AlgEquiv.uniqueProd_apply, AlgHom.fst_prod, StarAlgHom.fst_prod, ContinuousAlgHom.coe_snd', instIsNoetherianRingProd, Subalgebra.mem_prod, AlgEquiv.prodUnique_symm_apply, Ideal.map_prodComm_prod, AlgEquiv.uniqueProd_symm_apply, Ideal.span_prod_le, AlgEquiv.sumArrowEquivProdArrow_apply, PrimeSpectrum.range_comap_fst, Subalgebra.prod_toSubmodule, AlgHom.prod_comp, AlgEquiv.prodCongr_symm_apply, ContinuousAlgHom.prod_apply, AlgHom.prod_apply, StarAlgHom.fst_apply, ContinuousAlgHom.snd_comp_prod, ContinuousAlgHom.coe_snd, instIsArtinianRingProd, Ideal.mem_prod, Subalgebra.coe_prod

RingEquiv

Definitions

Name	Category	Theorems
prodComm 📖	CompOp	5 math math: coe_prodComm_symm, snd_comp_coe_prodComm, coe_prodComm, Ideal.map_prodComm_prod, fst_comp_coe_prodComm
prodProdProdComm 📖	CompOp	5 math math: prodProdProdComm_apply, prodProdProdComm_toMulEquiv, prodProdProdComm_symm, prodProdProdComm_toEquiv, prodProdProdComm_toAddEquiv
prodZeroRing 📖	CompOp	2 math math: prodZeroRing_symm_apply, prodZeroRing_apply
zeroRingProd 📖	CompOp	2 math math: zeroRingProd_symm_apply, zeroRingProd_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_prodComm 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike prodComm	—	—
coe_prodComm_symm 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike symm prodComm	—	—
fst_comp_coe_prodComm 📖	mathematical	—	RingHom.comp Prod.instNonAssocSemiring RingHom.fst RingHomClass.toRingHom RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass prodComm RingHom.snd	—	RingHom.ext RingEquivClass.toRingHomClass instRingEquivClass
prodProdProdComm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike prodProdProdComm	—	—
prodProdProdComm_symm 📖	mathematical	—	symm Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd prodProdProdComm	—	—
prodProdProdComm_toAddEquiv 📖	mathematical	—	AddEquivClass.toAddEquiv RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd instEquivLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne RingEquivClass.toAddEquivClass instRingEquivClass prodProdProdComm AddEquiv.prodProdProdComm	—	RingEquivClass.toAddEquivClass instRingEquivClass
prodProdProdComm_toEquiv 📖	mathematical	—	EquivLike.toEquiv RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd instEquivLike prodProdProdComm Equiv.prodProdProdComm	—	—
prodProdProdComm_toMulEquiv 📖	mathematical	—	MulEquivClass.toMulEquiv RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd instEquivLike MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass RingEquivClass.toMulEquivClass instRingEquivClass prodProdProdComm MulEquiv.prodProdProdComm	—	RingEquivClass.toMulEquivClass instRingEquivClass
prodZeroRing_apply 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instMul Distrib.toAdd Prod.instAdd EquivLike.toFunLike instEquivLike prodZeroRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
prodZeroRing_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike symm prodZeroRing	—	—
snd_comp_coe_prodComm 📖	mathematical	—	RingHom.comp Prod.instNonAssocSemiring RingHom.snd RingHomClass.toRingHom RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass prodComm RingHom.fst	—	RingHom.ext RingEquivClass.toRingHomClass instRingEquivClass
zeroRingProd_apply 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instMul Distrib.toAdd Prod.instAdd EquivLike.toFunLike instEquivLike zeroRingProd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
zeroRingProd_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike symm zeroRingProd	—	—

RingHom

Definitions

Name	Category	Theorems
fst 📖	CompOp	26 math math: PrimeSpectrum.primeSpectrumProd_symm_inl, Ideal.map_fst_prod, prod_unique, RingEquiv.snd_comp_coe_prodComm, Subsemiring.prod_top, PrimeSpectrum.isClosedEmbedding_comap_fst, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, Ideal.fst_comp_quotientMulEquivQuotientProd, coe_fst, prodMap_def, fst_comp_prod, Ideal.ideal_prod_eq, Subsemiring.range_fst, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, Subring.prod_top, AlgebraicGeometry.coprodSpec_inl_assoc, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, instRingHomSurjectiveProdFst, AlgebraicGeometry.coprodSpec_inl, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, Subring.range_fst, IsLocalization.away_fst, Ideal.fst_comp_quotientInfEquivQuotientProd, PrimeSpectrum.range_comap_fst, RingEquiv.fst_comp_coe_prodComm
prod 📖	CompOp	7 math math: snd_comp_prod, prod_unique, prod_comp_prodMap, prodMap_def, fst_comp_prod, prod_bijective_of_isIdempotentElem, prod_apply
prodMap 📖	CompOp	3 math math: prod_comp_prodMap, prodMap_def, coe_prodMap
snd 📖	CompOp	26 math math: Subring.range_snd, PrimeSpectrum.isClosedEmbedding_comap_snd, snd_comp_prod, AlgebraicGeometry.coprodSpec_inr, Subring.top_prod, prod_unique, RingEquiv.snd_comp_coe_prodComm, instRingHomSurjectiveProdSnd, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, IsLocalization.away_snd, PrimeSpectrum.primeSpectrumProd_symm_inr, prodMap_def, Ideal.ideal_prod_eq, Ideal.map_snd_prod, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, PrimeSpectrum.range_comap_snd, Ideal.snd_comp_quotientMulEquivQuotientProd, Subsemiring.range_snd, AlgebraicGeometry.coprodSpec_inr_assoc, coe_snd, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, Subsemiring.top_prod, Ideal.snd_comp_quotientInfEquivQuotientProd, RingEquiv.fst_comp_coe_prodComm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_fst 📖	mathematical	—	DFunLike.coe RingHom Prod.instNonAssocSemiring instFunLike fst	—	—
coe_prodMap 📖	mathematical	—	DFunLike.coe RingHom Prod.instNonAssocSemiring instFunLike prodMap	—	—
coe_snd 📖	mathematical	—	DFunLike.coe RingHom Prod.instNonAssocSemiring instFunLike snd	—	—
fst_comp_prod 📖	mathematical	—	comp Prod.instNonAssocSemiring fst prod	—	ext
instRingHomSurjectiveProdFst 📖	mathematical	—	RingHomSurjective Prod.instSemiring fst Semiring.toNonAssocSemiring	—	—
instRingHomSurjectiveProdSnd 📖	mathematical	—	RingHomSurjective Prod.instSemiring snd Semiring.toNonAssocSemiring	—	—
prodMap_def 📖	mathematical	—	prodMap prod Prod.instNonAssocSemiring comp fst snd	—	—
prod_apply 📖	mathematical	—	DFunLike.coe RingHom Prod.instNonAssocSemiring instFunLike prod	—	—
prod_comp_prodMap 📖	mathematical	—	comp Prod.instNonAssocSemiring prodMap prod	—	—
prod_unique 📖	mathematical	—	prod comp Prod.instNonAssocSemiring fst snd	—	ext
snd_comp_prod 📖	mathematical	—	comp Prod.instNonAssocSemiring snd prod	—	ext

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
false_of_nontrivial_of_product_domain 📖	—	—	—	—	NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero IsDomain.to_noZeroDivisors mul_one MulZeroClass.mul_zero Prod.mk_eq_zero zero_ne_one NeZero.one

---

← Back to Index