Prod

📁 Source: Mathlib/RingTheory/Ideal/Prod.lean

Statistics

Metric	Count
Definitions `idealProdEquiv`, `prod`	2
Theorems `coe_prod`, `idealProdEquiv_symm_apply`, `ideal_prod_eq`, `ideal_prod_prime`, `ideal_prod_prime_aux`, `isPrime_ideal_prod_top`, `isPrime_ideal_prod_top'`, `isPrime_of_isPrime_prod_top`, `isPrime_of_isPrime_prod_top'`, `map_fst_prod`, `map_prodComm_prod`, `map_snd_prod`, `mem_prod`, `prod_bot_bot`, `prod_eq_bot_iff`, `prod_eq_top_iff`, `prod_inj`, `prod_mono`, `prod_mono_left`, `prod_mono_right`, `prod_top_top`, `span_prod`, `span_prod_le`, `instIsPrincipalIdealRingProd`	24
Total	26

Ideal

Definitions

Name	Category	Theorems
`idealProdEquiv` 📖	CompOp	1 math math: `idealProdEquiv_symm_apply`
`prod` 📖	CompOp	22 math math: `isPrime_ideal_prod_top`, `span_prod`, `map_fst_prod`, `PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal`, `ideal_prod_prime`, `prod_inj`, `prod_bot_bot`, `isPrime_ideal_prod_top'`, `prod_mono_left`, `idealProdEquiv_symm_apply`, `ideal_prod_eq`, `map_snd_prod`, `prod_mono_right`, `prod_mono`, `prod_eq_top_iff`, `prod_eq_bot_iff`, `coe_prod`, `prod_top_top`, `PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal`, `map_prodComm_prod`, `span_prod_le`, `mem_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_prod` 📖	mathematical	—	`SetLike.coe` `Ideal` `Prod.instSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `prod` `SProd.sprod` `Set` `Set.instSProd`	—	—
`idealProdEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Ideal` `Prod.instSemiring` `Prod.instLE_mathlib` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLikeOrderIso` `OrderIso.symm` `idealProdEquiv` `prod`	—	—
`ideal_prod_eq` 📖	mathematical	—	`prod` `map` `RingHom` `Prod.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `Prod.instSemiring` `RingHom.instFunLike` `RingHom.fst` `RingHom.snd`	—	`ext` `mem_prod` `mem_map_iff_of_surjective` `RingHom.instRingHomClass` `Prod.fst_surjective` `Zero.instNonempty` `Prod.snd_surjective` `one_mul` `MulZeroClass.zero_mul` `add_zero` `zero_add` `add_mem` `mul_mem_left`
`ideal_prod_prime` 📖	mathematical	—	`IsPrime` `Prod.instSemiring` `prod` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`ideal_prod_eq` `ideal_prod_prime_aux` `isPrime_of_isPrime_prod_top'` `isPrime_of_isPrime_prod_top` `isPrime_ideal_prod_top` `isPrime_ideal_prod_top'`
`ideal_prod_prime_aux` 📖	mathematical	—	`Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `mul_one` `MulZeroClass.mul_zero` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`
`isPrime_ideal_prod_top` 📖	mathematical	—	`IsPrime` `Prod.instSemiring` `prod` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`IsPrime.ne_top` `IsPrime.mem_or_mem`
`isPrime_ideal_prod_top'` 📖	mathematical	—	`IsPrime` `Prod.instSemiring` `prod` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_prodComm_prod` `map_isPrime_of_equiv` `isPrime_ideal_prod_top`
`isPrime_of_isPrime_prod_top` 📖	mathematical	—	`IsPrime`	—	`Mathlib.Tactic.Contrapose.contrapose₃` `prod_top_top` `isPrime_iff` `mul_one` `mem_prod` `IsPrime.mem_or_mem`
`isPrime_of_isPrime_prod_top'` 📖	mathematical	—	`IsPrime`	—	`isPrime_of_isPrime_prod_top` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_prodComm_prod` `map_isPrime_of_equiv`
`map_fst_prod` 📖	mathematical	—	`map` `RingHom` `Prod.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `Prod.instSemiring` `RingHom.instFunLike` `RingHom.fst` `prod`	—	`ext` `mem_map_iff_of_surjective` `RingHom.instRingHomClass` `Prod.fst_surjective` `Zero.instNonempty` `zero_mem`
`map_prodComm_prod` 📖	mathematical	—	`map` `RingHom` `Prod.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `Prod.instSemiring` `RingHom.instFunLike` `RingHomClass.toRingHom` `RingEquiv` `Prod.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Prod.instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.prodComm` `prod`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `ideal_prod_eq` `map_map` `RingEquiv.fst_comp_coe_prodComm` `map_snd_prod` `RingEquiv.snd_comp_coe_prodComm` `map_fst_prod`
`map_snd_prod` 📖	mathematical	—	`map` `RingHom` `Prod.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `Prod.instSemiring` `RingHom.instFunLike` `RingHom.snd` `prod`	—	`ext` `mem_map_iff_of_surjective` `RingHom.instRingHomClass` `Prod.snd_surjective` `Zero.instNonempty` `zero_mem`
`mem_prod` 📖	mathematical	—	`Ideal` `Prod.instSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `prod`	—	—
`prod_bot_bot` 📖	mathematical	—	`prod` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Prod.instSemiring`	—	`SetLike.coe_injective` `Set.singleton_prod_singleton`
`prod_eq_bot_iff` 📖	mathematical	—	`prod` `Bot.bot` `Ideal` `Prod.instSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`prod_bot_bot`
`prod_eq_top_iff` 📖	mathematical	—	`prod` `Top.top` `Ideal` `Prod.instSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`prod_top_top`
`prod_inj` 📖	mathematical	—	`prod`	—	`OrderIso.injective`
`prod_mono` 📖	mathematical	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Prod.instSemiring` `prod`	—	`Set.prod_mono`
`prod_mono_left` 📖	mathematical	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Prod.instSemiring` `prod`	—	`Set.prod_mono_left`
`prod_mono_right` 📖	mathematical	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Prod.instSemiring` `prod`	—	`Set.prod_mono_right`
`prod_top_top` 📖	mathematical	—	`prod` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Prod.instSemiring`	—	`ext`
`span_prod` 📖	mathematical	`Set.Nonempty`	`span` `Prod.instSemiring` `SProd.sprod` `Set` `Set.instSProd` `prod`	—	`ideal_prod_eq` `map_span` `RingHom.instRingHomClass` `Set.image_congr` `Set.fst_image_prod` `Set.snd_image_prod` `Set.prod_empty` `span_empty` `prod_bot_bot`
`span_prod_le` 📖	mathematical	—	`Ideal` `Prod.instSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `span` `SProd.sprod` `Set` `Set.instSProd` `prod`	—	`ideal_prod_eq` `map_span` `RingHom.instRingHomClass` `prod_mono` `span_mono` `Set.fst_image_prod_subset` `Set.snd_image_prod_subset`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsPrincipalIdealRingProd` 📖	mathematical	—	`IsPrincipalIdealRing` `Prod.instSemiring`	—	`Ideal.ideal_prod_eq` `IsPrincipalIdealRing.principal` `Submodule.IsPrincipal.span_singleton_generator` `Ideal.span.eq_1` `Ideal.span_prod` `Set.singleton_prod_singleton`

---

← Back to Index