Pi

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

Statistics

Metric	Count
Definitions	0
Theorems noZeroSMulDivisors, noZeroSMulDivisors	2
Total	2

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
noZeroSMulDivisors 📖	mathematical	—	NoZeroSMulDivisors MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	Pi.noZeroSMulDivisors

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
noZeroSMulDivisors 📖	mathematical	NoZeroSMulDivisors MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid	instZero instSMul	—	smul_eq_zero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors IsDomain.toIsCancelMulZero

---

← Back to Index