Pi

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

Statistics

Metric	Count
Definitions pi	1
Theorems coe_pi, mem_pi, pi_mono, pi_toSubmodule, pi_toSubsemiring, pi_top	6
Total	7

Subalgebra

Definitions

Name	Category	Theorems
pi 📖	CompOp	6 math math: pi_top, pi_mono, pi_toSubsemiring, coe_pi, mem_pi, pi_toSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pi 📖	mathematical	—	SetLike.coe Subalgebra Pi.semiring Pi.algebra instSetLike pi AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddSubmonoid.toAddSubsemigroup Submodule.toAddSubmonoid CommSemiring.toSemiring Pi.module Algebra.toModule Submodule.pi DFunLike.coe OrderEmbedding Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding toSubmodule	—	—
mem_pi 📖	mathematical	—	Subalgebra Pi.semiring Pi.algebra SetLike.instMembership instSetLike pi	—	—
pi_mono 📖	mathematical	Subalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder	Pi.semiring Pi.algebra pi	—	Set.pi_mono
pi_toSubmodule 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Pi.semiring Pi.algebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding toSubmodule pi Submodule.pi	—	—
pi_toSubsemiring 📖	mathematical	—	toSubsemiring Pi.semiring Pi.algebra pi Semiring.toNonAssocSemiring MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MulOne.toMul MulOneClass.toMulOne AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddSubmonoid.toAddSubsemigroup Submodule.toAddSubmonoid CommSemiring.toSemiring Pi.module Algebra.toModule Submodule.pi DFunLike.coe OrderEmbedding Subalgebra Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding toSubmodule	—	—
pi_top 📖	mathematical	—	pi Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Pi.semiring Pi.algebra	—	SetLike.coe_injective Set.pi_univ

---

← Back to Index