Field

📁 Source: Mathlib/Algebra/Module/Torsion/Field.lean

Statistics

Metric	Count
Definitions	0
Theorems to_moduleIsTorsionFree	1
Total	1

DivisionSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_moduleIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree toSemiring	—	inv_smul_smul₀ IsRegular.ne_zero GroupWithZero.toNontrivial

---

← Back to Index