Documentation Verification Report

Prod

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

Statistics

Metric	Count
Definitions `instCommMonoidWithZero`, `instMonoidWithZero`, `instMulZeroClass`, `instMulZeroOneClass`, `instSemigroupWithZero`, `divMonoidWithZeroHom`, `mulMonoidWithZeroHom`	7
Theorems `toMonoidWithZeroHom_withZeroUnitsEquiv`, `divMonoidWithZeroHom_apply`, `mulMonoidWithZeroHom_apply`	3
Total	10

Prod

Definitions

Name	Category	Theorems
`instCommMonoidWithZero` 📖	CompOp	—
`instMonoidWithZero` 📖	CompOp	—
`instMulZeroClass` 📖	CompOp	—
`instMulZeroOneClass` 📖	CompOp	44 math math: `NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace`, `NumberField.mixedEmbedding.normAtAllPlaces_apply`, `NumberField.mixedEmbedding.norm_eq_zero_iff'`, `NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst`, `NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isComplex`, `NumberField.mixedEmbedding.norm_unit_smul`, `NumberField.mixedEmbedding.norm_eq_norm`, `smulMonoidWithZeroHom_apply`, `NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le`, `NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion`, `NumberField.mixedEmbedding.normAtPlace_apply_of_isReal`, `NumberField.mixedEmbedding.fundamentalCone.norm_pos_of_mem`, `NumberField.mixedEmbedding.convexBodySumFun_apply`, `NumberField.mixedEmbedding.fundamentalCone.mem_normLeOne`, `NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis`, `mulMonoidWithZeroHom_apply`, `NumberField.mixedEmbedding.normAtPlace_add_le`, `NumberField.mixedEmbedding.norm_nonneg`, `NumberField.mixedEmbedding.norm_smul`, `NumberField.mixedEmbedding.continuous_norm`, `NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces`, `NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isReal`, `NumberField.mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem`, `NumberField.mixedEmbedding.normAtPlace_neg`, `NumberField.mixedEmbedding.continuous_normAtPlace`, `NumberField.mixedEmbedding.normAtPlace_apply`, `NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex`, `NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff`, `NumberField.mixedEmbedding.logMap_apply`, `NumberField.mixedEmbedding.fundamentalCone.intNorm_coe`, `NumberField.mixedEmbedding.norm_eq_zero_iff`, `NumberField.mixedEmbedding.normAtPlace_nonneg`, `NumberField.mixedEmbedding.normAtPlace_negAt`, `NumberField.mixedEmbedding.normAtPlace_smul`, `divMonoidWithZeroHom_apply`, `NumberField.mixedEmbedding.norm_real`, `NumberField.mixedEmbedding.norm_negAt`, `NumberField.mixedEmbedding.norm_unit`, `NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace`, `NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace`, `NumberField.mixedEmbedding.norm_apply`, `NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne`, `NumberField.mixedEmbedding.normAtPlace_real`, `NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply`
`instSemigroupWithZero` 📖	CompOp	—

WithZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMonoidWithZeroHom_withZeroUnitsEquiv` 📖	mathematical	—	`MonoidWithZeroHomClass.toMonoidWithZeroHom` `MulEquiv` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulZeroClass.toMul` `instMulZeroClass` `Units.instMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `instMulZeroOneClass` `Units.instMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.toMonoidWithZeroHomClass` `MulEquiv.instMulEquivClass` `withZeroUnitsEquiv` `DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZeroHom` `Equiv.instEquivLike` `lift'` `Units.coeHom`	—	`MulEquivClass.toMonoidWithZeroHomClass` `MulEquiv.instMulEquivClass`

(root)

Definitions

Name	Category	Theorems
`divMonoidWithZeroHom` 📖	CompOp	1 math math: `divMonoidWithZeroHom_apply`
`mulMonoidWithZeroHom` 📖	CompOp	1 math math: `mulMonoidWithZeroHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divMonoidWithZeroHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Prod.instMulZeroOneClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `MonoidWithZeroHom.funLike` `divMonoidWithZeroHom` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `Prod.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `MonoidHom.toOneHom` `divMonoidHom`	—	—
`mulMonoidWithZeroHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Prod.instMulZeroOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `mulMonoidWithZeroHom` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `Prod.instMulOneClass` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `CommMonoidWithZero.toCommMonoid` `MonoidHom.toOneHom` `mulMonoidHom`	—	—

---

← Back to Index