DedekindFinite

📁 Source: Mathlib/GroupTheory/DedekindFinite.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsDedekindFiniteMonoidOfFinite	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsDedekindFiniteMonoidOfFinite 📖	mathematical	—	IsDedekindFiniteMonoid MulOneClass.toMulOne Monoid.toMulOneClass	—	Finite.surjective_of_injective isLeftRegular_of_mul_eq_one left_inv_eq_right_inv

---

← Back to Index