Documentation Verification Report

Pi

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

Statistics

Metric	Count
Definitions `funUnique`, `piCongrLeft`, `piCongrLeft'`, `piCongrRight`, `piMulOpposite`, `sumArrowEquivProdArrow`, `compLeft`, `algebra`, `algHom`, `algebra`, `constAlgHom`, `evalAlgHom`, `instAlgebraForall`	13
Theorems `funUnique_apply`, `funUnique_symm_apply`, `piCongrLeft'_apply`, `piCongrLeft'_symm_apply`, `piCongrLeft_apply`, `piCongrLeft_symm_apply`, `piCongrRight_apply`, `piCongrRight_refl`, `piCongrRight_symm`, `piCongrRight_trans`, `sumArrowEquivProdArrow_apply`, `sumArrowEquivProdArrow_symm_apply_inr`, `compLeft_apply`, `algHom_apply`, `algHom_comp`, `algHom_evalAlgHom`, `algebraMap_apply`, `algebraMap_def`, `constAlgHom_apply`, `constAlgHom_eq_algebra_ofId`, `constRingHom_eq_algebraMap`, `evalAlgHom_apply`	22
Total	35

AlgEquiv

Definitions

Name	Category	Theorems
`funUnique` 📖	CompOp	2 math math: `funUnique_apply`, `funUnique_symm_apply`
`piCongrLeft` 📖	CompOp	2 math math: `piCongrLeft_apply`, `piCongrLeft_symm_apply`
`piCongrLeft'` 📖	CompOp	2 math math: `piCongrLeft'_apply`, `piCongrLeft'_symm_apply`
`piCongrRight` 📖	CompOp	4 math math: `piCongrRight_refl`, `piCongrRight_trans`, `piCongrRight_symm`, `piCongrRight_apply`
`piMulOpposite` 📖	CompOp	—
`sumArrowEquivProdArrow` 📖	CompOp	2 math math: `sumArrowEquivProdArrow_symm_apply_inr`, `sumArrowEquivProdArrow_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`funUnique_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Pi.semiring` `Function.algebra` `instFunLike` `funUnique` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.funUnique`	—	—
`funUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Pi.semiring` `Function.algebra` `instFunLike` `symm` `funUnique` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.funUnique`	—	—
`piCongrLeft'_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Pi.semiring` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Pi.algebra` `instFunLike` `piCongrLeft'` `Equiv.piCongrLeft'`	—	—
`piCongrLeft'_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Pi.semiring` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Pi.algebra` `instFunLike` `symm` `piCongrLeft'` `Equiv.piCongrLeft'`	—	—
`piCongrLeft_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Pi.semiring` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Pi.algebra` `instFunLike` `piCongrLeft` `Equiv.piCongrLeft`	—	—
`piCongrLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Pi.semiring` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Pi.algebra` `instFunLike` `symm` `piCongrLeft` `Equiv.symm` `Equiv.piCongrLeft`	—	—
`piCongrRight_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Pi.semiring` `Pi.algebra` `instFunLike` `piCongrRight`	—	—
`piCongrRight_refl` 📖	mathematical	—	`piCongrRight` `refl` `Pi.semiring` `Pi.algebra`	—	—
`piCongrRight_symm` 📖	mathematical	—	`symm` `Pi.semiring` `Pi.algebra` `piCongrRight`	—	—
`piCongrRight_trans` 📖	mathematical	—	`trans` `Pi.semiring` `Pi.algebra` `piCongrRight`	—	—
`sumArrowEquivProdArrow_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Pi.semiring` `Prod.instSemiring` `Function.algebra` `Prod.algebra` `instFunLike` `sumArrowEquivProdArrow` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.sumArrowEquivProdArrow`	—	—
`sumArrowEquivProdArrow_symm_apply_inr` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Prod.instSemiring` `Pi.semiring` `Prod.algebra` `Function.algebra` `instFunLike` `symm` `sumArrowEquivProdArrow` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.sumArrowEquivProdArrow`	—	—

AlgHom

Definitions

Name	Category	Theorems
`compLeft` 📖	CompOp	1 math math: `compLeft_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeft_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Pi.semiring` `Function.algebra` `funLike` `compLeft`	—	—

Function

Definitions

Name	Category	Theorems
`algebra` 📖	CompOp	18 math math: `Pi.comul_eq_adjoint`, `ContMDiffMap.coeFnAlgHom_apply`, `Polynomial.aeval_fn_apply`, `Algebra.TensorProduct.piScalarRight_tmul`, `Pi.counit_eq_adjoint`, `ContinuousMap.coeFnAlgHom_apply`, `AlgEquiv.sumArrowEquivProdArrow_symm_apply_inr`, `AlgEquiv.funUnique_apply`, `LocallyConstant.coeFnAlgHom_apply`, `AlgHom.compLeft_apply`, `Matrix.algebraMap_eq_diagonal`, `Matrix.diagonalAlgHom_apply`, `LocallyConstant.coe_algebraMap`, `AlgEquiv.sumArrowEquivProdArrow_apply`, `AlgEquiv.funUnique_symm_apply`, `Algebra.TensorProduct.piScalarRight_tmul_apply`, `MeasureTheory.SimpleFunc.coe_algebraMap`, `Matrix.algebraMap_eq_diagonalRingHom`

Pi

Definitions

Name	Category	Theorems
`algHom` 📖	CompOp	4 math math: `algHom_comp`, `algHom_apply`, `algHom_evalAlgHom`, `Polynomial.aeval_pi`
`algebra` 📖	CompOp	52 math math: `AlgEquiv.piCongrRight_refl`, `constAlgHom_apply`, `Localization.algebraMap_injective_of_span_eq_top`, `algebraMap_apply`, `Subalgebra.pi_top`, `AlgEquiv.piCongrRight_trans`, `algHom_comp`, `Algebra.TensorProduct.piRightHom_mul`, `Algebra.FormallyEtale.instForallOfFinite`, `Algebra.FormallyUnramified.instForall`, `spectrum_eq`, `Polynomial.aeval_pi_apply`, `AlgEquiv.piCongrRight_symm`, `IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite`, `IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing`, `algHom_apply`, `CFC.rpow_eq_rpow_pi`, `AlgEquiv.piCongrLeft'_apply`, `AlgEquiv.piCongrLeft_apply`, `algHom_evalAlgHom`, `IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed`, `Algebra.FormallyUnramified.pi_iff`, `NumberField.InfinitePlace.denseRange_algebraMap_pi`, `Subalgebra.pi_mono`, `IsSemisimpleModule.exists_end_algEquiv`, `Subalgebra.pi_toSubsemiring`, `Algebra.TensorProduct.piRight_tmul`, `Matrix.piAlgEquiv_symm_apply`, `Algebra.FormallySmooth.instForallOfFinite`, `Algebra.FormallyEtale.pi_iff`, `AlgCat.instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra`, `Subalgebra.coe_pi`, `cfc_map_pi`, `IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end`, `Algebra.FormallySmooth.pi_iff`, `AlgEquiv.piCongrLeft_symm_apply`, `IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing`, `AlgEquiv.piCongrRight_apply`, `Algebra.FinitePresentation.pi`, `CFC.rpow_map_pi`, `IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite`, `Polynomial.aeval_pi`, `Subalgebra.mem_pi`, `Polynomial.aeval_pi_apply₂`, `evalStarAlgHom_apply`, `constAlgHom_eq_algebra_ofId`, `evalAlgHom_apply`, `constRingHom_eq_algebraMap`, `algebraMap_def`, `Subalgebra.pi_toSubmodule`, `AlgEquiv.piCongrLeft'_symm_apply`, `Matrix.piAlgEquiv_apply`
`constAlgHom` 📖	CompOp	2 math math: `constAlgHom_apply`, `constAlgHom_eq_algebra_ofId`
`evalAlgHom` 📖	CompOp	3 math math: `algHom_evalAlgHom`, `evalAlgHom_apply`, `AlgHom.eq_piEvalAlgHom`
`instAlgebraForall` 📖	CompOp	2 math math: `TensorProduct.piScalarRight_symm_algebraMap`, `IsLocalization.instForallPiUniv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `semiring` `algebra` `AlgHom.funLike` `algHom`	—	—
`algHom_comp` 📖	mathematical	—	`AlgHom.comp` `semiring` `algebra` `algHom`	—	—
`algHom_evalAlgHom` 📖	mathematical	—	`algHom` `semiring` `algebra` `evalAlgHom` `AlgHom.id`	—	—
`algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `semiring` `RingHom.instFunLike` `algebraMap` `algebra`	—	—
`algebraMap_def` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `semiring` `RingHom.instFunLike` `algebraMap` `algebra`	—	—
`constAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `semiring` `algebra` `AlgHom.funLike` `constAlgHom`	—	—
`constAlgHom_eq_algebra_ofId` 📖	mathematical	—	`constAlgHom` `CommSemiring.toSemiring` `Algebra.id` `Algebra.ofId` `semiring` `algebra`	—	—
`constRingHom_eq_algebraMap` 📖	mathematical	—	`constRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebraMap` `semiring` `algebra` `Algebra.id`	—	—
`evalAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `semiring` `algebra` `AlgHom.funLike` `evalAlgHom`	—	—

---

← Back to Index