Documentation Verification Report

Pi

📁 Source: Mathlib/LinearAlgebra/Quotient/Pi.lean

Statistics

Metric	Count
Definitions `piQuotientLift`, `quotientPi`, `quotientPiLift`, `invFun`, `toFun`	5
Theorems `piQuotientLift_mk`, `piQuotientLift_single`, `quotientPiLift_mk`, `quotientPi_apply`, `left_inv`, `map_add`, `map_smul`, `right_inv`, `quotientPi_symm_apply`	9
Total	14

Submodule

Definitions

Name	Category	Theorems
`piQuotientLift` 📖	CompOp	3 math math: `quotientPi_symm_apply`, `piQuotientLift_single`, `piQuotientLift_mk`
`quotientPi` 📖	CompOp	2 math math: `quotientPi_apply`, `quotientPi_symm_apply`
`quotientPiLift` 📖	CompOp	2 math math: `quotientPi_apply`, `quotientPiLift_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`piQuotientLift_mk` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `comap` `RingHom.id` `Semiring.toNonAssocSemiring`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HasQuotient.Quotient` `Submodule` `AddCommGroup.toAddCommMonoid` `hasQuotient` `CommRing.toRing` `Pi.addCommMonoid` `Quotient.addCommGroup` `Pi.module` `Quotient.module` `LinearMap.instFunLike` `piQuotientLift` `LinearEquiv` `RingHomInvPair.ids` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearMap.lsum`	—	`RingHomInvPair.ids` `smulCommClass_self` `piQuotientLift.eq_1` `RingHomCompTriple.ids` `LinearMap.lsum_apply` `LinearMap.sum_apply` `mkQ_apply` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr`
`piQuotientLift_single` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `comap` `RingHom.id` `Semiring.toNonAssocSemiring`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HasQuotient.Quotient` `Submodule` `AddCommGroup.toAddCommMonoid` `hasQuotient` `CommRing.toRing` `Pi.addCommMonoid` `Quotient.addCommGroup` `Pi.module` `Quotient.module` `LinearMap.instFunLike` `piQuotientLift` `Pi.single` `Quotient.instZeroQuotient` `Ring.toSemiring` `mapQ`	—	`RingHomCompTriple.ids` `LinearMap.sum_apply` `Finset.sum_congr` `Finset.sum_eq_single` `Pi.single_eq_of_ne` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.mem_univ` `Pi.single_eq_same`
`quotientPiLift_mk` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HasQuotient.Quotient` `Submodule` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.module` `hasQuotient` `CommRing.toRing` `Pi.addCommGroup` `pi` `Set.univ` `Quotient.addCommGroup` `Quotient.module` `LinearMap.instFunLike` `quotientPiLift`	—	—
`quotientPi_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `HasQuotient.Quotient` `Submodule` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.module` `hasQuotient` `CommRing.toRing` `Pi.addCommGroup` `pi` `Set.univ` `Quotient.addCommGroup` `Quotient.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `quotientPi` `LinearMap` `Ring.toSemiring` `LinearMap.instFunLike` `quotientPiLift` `mkQ`	—	`RingHomInvPair.ids`
`quotientPi_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `HasQuotient.Quotient` `Submodule` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.module` `hasQuotient` `CommRing.toRing` `Pi.addCommGroup` `pi` `Set.univ` `Quotient.addCommGroup` `Quotient.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `quotientPi` `LinearMap` `LinearMap.instFunLike` `piQuotientLift` `LinearMap.single`	—	`RingHomInvPair.ids`

Submodule.quotientPi_aux

Definitions

Name	Category	Theorems
`invFun` 📖	CompOp	2 math math: `left_inv`, `right_inv`
`toFun` 📖	CompOp	4 math math: `map_smul`, `map_add`, `left_inv`, `right_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_inv` 📖	mathematical	—	`HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.module` `Submodule.hasQuotient` `CommRing.toRing` `Pi.addCommGroup` `Submodule.pi` `Set.univ` `invFun` `toFun`	—	`Submodule.Quotient.induction_on` `Submodule.mkQ_apply` `RingHomInvPair.ids` `smulCommClass_self` `Pi.smulCommClass` `LinearMap.lsum_single` `LinearMap.id_apply`
`map_add` 📖	mathematical	—	`toFun` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.module` `Submodule.hasQuotient` `CommRing.toRing` `Pi.addCommGroup` `Submodule.pi` `Set.univ` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Submodule.Quotient.addCommGroup` `Pi.instAdd`	—	`LinearMap.map_add` `Eq.ge` `Submodule.ker_mkQ`
`map_smul` 📖	mathematical	—	`toFun` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.module` `Submodule.hasQuotient` `CommRing.toRing` `Pi.addCommGroup` `Submodule.pi` `Set.univ` `Submodule.Quotient.instSMul` `Pi.instSMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.id`	—	`LinearMap.map_smul` `Eq.ge` `Submodule.ker_mkQ`
`right_inv` 📖	mathematical	—	`HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.module` `Submodule.hasQuotient` `CommRing.toRing` `Pi.addCommGroup` `Submodule.pi` `Set.univ` `invFun` `toFun`	—	`Function.rightInverse_iff_comp` `RingHomCompTriple.ids` `LinearMap.coe_comp` `LinearMap.id_coe` `LinearMap.pi_ext` `Finite.of_fintype` `Submodule.Quotient.induction_on` `LinearMap.comp_apply` `Submodule.piQuotientLift_single` `Submodule.mapQ_apply` `LinearMap.id_apply` `Pi.single_eq_same` `Pi.single_eq_of_ne` `Submodule.Quotient.mk_zero`

---

← Back to Index