Documentation Verification Report

Card

📁 Source: Mathlib/Algebra/Module/Card.lean

Statistics

MetricCount
Definitions0
Theoremsmk_le_of_module
1
Total1

Cardinal

Theorems

NameKindAssumesProvesValidatesDepends On
mk_le_of_module 📖mathematicalCardinal
instLE
lift
exists_ne
smul_left_injective
IsDomain.toIsCancelMulZero
lift_mk_le_lift_mk_of_injective

---

← Back to Index