Documentation Verification Report

Pi

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

Statistics

Metric	Count
Definitions `single`, `commMonoidWithZero`, `monoidWithZero`, `mulZeroClass`, `mulZeroOneClass`, `semigroupWithZero`	6
Theorems `single_apply`, `single_mul`, `single_mul_left`, `single_mul_left_apply`, `single_mul_right`, `single_mul_right_apply`	6
Total	12

MulHom

Definitions

Name	Category	Theorems
`single` 📖	CompOp	1 math math: `single_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`single_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `MulZeroClass.toMul` `Pi.instMul` `funLike` `single` `Pi.single` `MulZeroClass.toZero`	—	—

Pi

Definitions

Name	Category	Theorems
`commMonoidWithZero` 📖	CompOp	—
`monoidWithZero` 📖	CompOp	1 math math: `Matrix.inv_diagonal`
`mulZeroClass` 📖	CompOp	—
`mulZeroOneClass` 📖	CompOp	41 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`, `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`, `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`, `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`
`semigroupWithZero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`single_mul` 📖	mathematical	—	`single` `MulZeroClass.toZero` `MulZeroClass.toMul` `instMul`	—	`MulHom.map_mul`
`single_mul_left` 📖	mathematical	—	`single` `MulZeroClass.toZero` `MulZeroClass.toMul` `instMul`	—	`single_mul_left_apply`
`single_mul_left_apply` 📖	mathematical	—	`single` `MulZeroClass.toZero` `MulZeroClass.toMul`	—	`apply_single` `MulZeroClass.zero_mul`
`single_mul_right` 📖	mathematical	—	`single` `MulZeroClass.toZero` `MulZeroClass.toMul` `instMul`	—	`single_mul_right_apply`
`single_mul_right_apply` 📖	mathematical	—	`single` `MulZeroClass.toZero` `MulZeroClass.toMul`	—	`apply_single` `MulZeroClass.mul_zero`

---

← Back to Index