Documentation Verification Report

Prod

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

Statistics

Metric	Count
Definitions `prodCongr`, `prodUnique`, `uniqueProd`, `fst`, `prod`, `prodEquiv`, `prodMap`, `snd`, `algebra`	9
Theorems `prodCongr_apply`, `prodCongr_symm_apply`, `prodUnique_apply`, `prodUnique_symm_apply`, `uniqueProd_apply`, `uniqueProd_symm_apply`, `coe_prod`, `fst_apply`, `fst_prod`, `prodEquiv_apply`, `prodEquiv_symm_apply`, `prod_apply`, `prod_comp`, `prod_fst_snd`, `snd_apply`, `snd_prod`, `algebraMap_apply`	17
Total	26

AlgEquiv

Definitions

Name	Category	Theorems
`prodCongr` 📖	CompOp	2 math math: `prodCongr_apply`, `prodCongr_symm_apply`
`prodUnique` 📖	CompOp	2 math math: `prodUnique_apply`, `prodUnique_symm_apply`
`uniqueProd` 📖	CompOp	2 math math: `uniqueProd_apply`, `uniqueProd_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodCongr_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Prod.instSemiring` `Prod.algebra` `instFunLike` `prodCongr` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.prodCongr` `EquivLike.toEquiv` `instEquivLike`	—	—
`prodCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Prod.instSemiring` `Prod.algebra` `instFunLike` `symm` `prodCongr` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.prodCongr` `EquivLike.toEquiv` `instEquivLike`	—	—
`prodUnique_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Prod.instSemiring` `Prod.algebra` `instFunLike` `prodUnique`	—	—
`prodUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Prod.instSemiring` `Prod.algebra` `instFunLike` `symm` `prodUnique` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`uniqueProd_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Prod.instSemiring` `Prod.algebra` `instFunLike` `uniqueProd`	—	—
`uniqueProd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Prod.instSemiring` `Prod.algebra` `instFunLike` `symm` `uniqueProd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—

AlgHom

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	5 math math: `ContinuousAlgHom.coe_fst`, `prodEquiv_symm_apply`, `fst_apply`, `prod_fst_snd`, `fst_prod`
`prod` 📖	CompOp	9 math math: `snd_prod`, `Polynomial.aeval_prod`, `coe_prod`, `ContinuousAlgHom.coe_prod`, `prod_fst_snd`, `prodEquiv_apply`, `fst_prod`, `prod_comp`, `prod_apply`
`prodEquiv` 📖	CompOp	2 math math: `prodEquiv_symm_apply`, `prodEquiv_apply`
`prodMap` 📖	CompOp	1 math math: `ContinuousAlgHom.coe_prodMap`
`snd` 📖	CompOp	5 math math: `snd_prod`, `prodEquiv_symm_apply`, `snd_apply`, `prod_fst_snd`, `ContinuousAlgHom.coe_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_prod` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Prod.instSemiring` `Prod.algebra` `funLike` `prod` `Pi.prod`	—	—
`fst_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Prod.instSemiring` `Prod.algebra` `funLike` `fst`	—	—
`fst_prod` 📖	mathematical	—	`comp` `Prod.instSemiring` `Prod.algebra` `fst` `prod`	—	`ext`
`prodEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `Prod.instSemiring` `Prod.algebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodEquiv` `prod`	—	—
`prodEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `Prod.instSemiring` `Prod.algebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `prodEquiv` `comp` `fst` `snd`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Prod.instSemiring` `Prod.algebra` `funLike` `prod`	—	—
`prod_comp` 📖	mathematical	—	`comp` `Prod.instSemiring` `Prod.algebra` `prod`	—	—
`prod_fst_snd` 📖	mathematical	—	`prod` `Prod.instSemiring` `Prod.algebra` `fst` `snd` `id`	—	—
`snd_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Prod.instSemiring` `Prod.algebra` `funLike` `snd`	—	—
`snd_prod` 📖	mathematical	—	`comp` `Prod.instSemiring` `Prod.algebra` `snd` `prod`	—	`ext`

Prod

Definitions

Name	Category	Theorems
`algebra` 📖	CompOp	76 math math: `ContinuousAlgHom.coe_fst`, `Algebra.TensorProduct.prodRight_tmul_fst`, `Unitization.splitMul_apply`, `IsIntegral.pair`, `Algebra.TensorProduct.prodRight_symm_tmul`, `StarAlgHom.prodEquiv_apply`, `AlgHom.snd_prod`, `AlgEquiv.prodQuotientOfIsIdempotentElem_apply`, `StarAlgHom.snd_apply`, `StarAlgHom.coe_prod`, `Subalgebra.prod_mono`, `Subalgebra.prod_inf_prod`, `Unitization.nnnorm_def`, `AlgEquiv.prodCongr_apply`, `cfc_map_prod`, `Algebra.IsIntegral.prod`, `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`, `spectrum_eq`, `AlgHom.coe_prod`, `IsIntegral.pair_iff`, `CFC.rpow_map_prod`, `StarAlgHom.snd_prod`, `AlgHom.fst_apply`, `Algebra.trace_prod`, `ContinuousAlgHom.coe_prod`, `DoubleCentralizer.algebraMap_toProd`, `AlgHom.snd_apply`, `Algebra.adjoin_inl_union_inr_eq_prod`, `StarAlgHom.prod_fst_snd`, `LinearMap.prodMapAlgHom_apply_apply`, `Unitization.norm_def`, `ContinuousAlgHom.coe_prodMap`, `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`, `ContinuousAlgHom.coe_prodMap'`, `AlgEquiv.prodQuotientOfIsIdempotentElem_apply_fst`, `StarAlgHom.prodEquiv_symm_apply`, `Subalgebra.prod_top`, `AlgHom.prodEquiv_apply`, `Algebra.trace_prod_apply`, `ContinuousAlgHom.fst_comp_prod`, `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'`, `Subalgebra.mem_prod`, `AlgEquiv.prodUnique_symm_apply`, `AlgEquiv.uniqueProd_symm_apply`, `AlgEquiv.sumArrowEquivProdArrow_apply`, `Subalgebra.prod_toSubmodule`, `AlgHom.prod_comp`, `AlgEquiv.prodCongr_symm_apply`, `ContinuousAlgHom.prod_apply`, `AlgHom.prod_apply`, `CFC.rpow_eq_rpow_prod`, `StarAlgHom.fst_apply`, `ContinuousAlgHom.snd_comp_prod`, `ContinuousAlgHom.coe_snd`, `Subalgebra.coe_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `algebra`	—	—

---

← Back to Index