Pi

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

Statistics

Metric	Count
Definitions toPi, toProd	2
Theorems quasispectrum_eq, spectrum_eq, quasispectrum_eq, spectrum_eq, isQuasiregular_pi_iff, isQuasiregular_prod_iff, mem_iff_of_isUnit	7
Total	9

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasispectrum_eq 📖	mathematical	—	quasispectrum nonUnitalRing module CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Set.iUnion	—	Set.ext CanLift.prf instCanLiftUnitsValIsUnit IsUnit.unit.congr_simp IsUnit.unit_of_val_units instIsEmptyFalse
spectrum_eq 📖	mathematical	—	spectrum ring algebra Ring.toSemiring Set.iUnion	—	compl_injective Set.compl_iUnion compl_compl Set.iInter_setOf

PreQuasiregular

Definitions

Name	Category	Theorems
toPi 📖	CompOp	—
toProd 📖	CompOp	—

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasispectrum_eq 📖	mathematical	—	quasispectrum instNonUnitalRing instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Set Set.instUnion	—	compl_injective Set.ext CanLift.prf instCanLiftUnitsValIsUnit IsUnit.unit.congr_simp IsUnit.unit_of_val_units instIsEmptyFalse
spectrum_eq 📖	mathematical	—	spectrum instRing algebra Ring.toSemiring Set Set.instUnion	—	compl_injective Set.compl_union compl_compl

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isQuasiregular_pi_iff 📖	mathematical	—	IsQuasiregular Pi.nonUnitalSemiring	—	isUnit_map_iff MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass isLocalHom_equiv
isQuasiregular_prod_iff 📖	mathematical	—	IsQuasiregular Prod.instNonUnitalSemiring	—	isUnit_map_iff MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass isLocalHom_equiv

quasispectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_iff_of_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	Set Set.instMembership quasispectrum IsQuasiregular NonUnitalRing.toNonUnitalSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing Units Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Units.instInv IsUnit.unit	—	—

---

← Back to Index