Finite

📁 Source: Mathlib/LinearAlgebra/Dimension/Torsion/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems finrank_eq_zero_iff_isTorsion, rank_eq_zero_iff_isTorsion	2
Total	2

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_eq_zero_iff_isTorsion 📖	mathematical	—	finrank CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid IsTorsion	—	rank_eq_zero_iff_isTorsion finrank_eq_rank Nat.cast_zero Cardinal.instCharZero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_eq_zero_iff_isTorsion 📖	mathematical	—	Module.rank CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Cardinal Cardinal.instZero Module.IsTorsion	—	Module.IsTorsion.eq_1 rank_eq_zero_iff IsDomain.to_noZeroDivisors IsDomain.toNontrivial

---

← Back to Index