NoncommRing

📁 Source: Mathlib/Tactic/NoncommRing.lean

Statistics

Metric	Count
Definitions noncomm_ring	1
Theorems mul_nat_lit_eq_nsmul, nat_lit_mul_eq_nsmul	2
Total	3

Mathlib.Tactic.NoncommRing

Definitions

Name	Category	Theorems
noncomm_ring 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_nat_lit_eq_nsmul 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	nsmul_eq_mul'
nat_lit_mul_eq_nsmul 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	nsmul_eq_mul

---

← Back to Index