Documentation Verification Report

Prod

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

Statistics

Metric	Count
Definitions `prod`	1
Theorems `coe_prod`, `mem_prod`, `prod_inf_prod`, `prod_mono`, `prod_toSubmodule`, `prod_top`	6
Total	7

Subalgebra

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	9 math math: `prod_mono`, `prod_inf_prod`, `FG.prod`, `Algebra.adjoin_inl_union_inr_eq_prod`, `Algebra.adjoin_prod_le`, `prod_top`, `mem_prod`, `prod_toSubmodule`, `coe_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_prod` 📖	mathematical	—	`SetLike.coe` `Subalgebra` `Prod.instSemiring` `Prod.algebra` `instSetLike` `prod` `SProd.sprod` `Set` `Set.instSProd`	—	—
`mem_prod` 📖	mathematical	—	`Subalgebra` `Prod.instSemiring` `Prod.algebra` `SetLike.instMembership` `instSetLike` `prod`	—	`Set.mem_prod`
`prod_inf_prod` 📖	mathematical	—	`Subalgebra` `Prod.instSemiring` `Prod.algebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `prod`	—	`SetLike.coe_injective` `Set.prod_inter_prod`
`prod_mono` 📖	mathematical	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instSemiring` `Prod.algebra` `prod`	—	`Set.prod_mono`
`prod_toSubmodule` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Subalgebra` `Prod.instSemiring` `Prod.algebra` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `toSubmodule` `prod` `Submodule.prod`	—	—
`prod_top` 📖	mathematical	—	`prod` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Prod.instSemiring` `Prod.algebra`	—	`ext`

---

← Back to Index