Card

📁 Source: Mathlib/LinearAlgebra/Quotient/Card.lean

Statistics

Metric	Count
Definitions	0
Theorems card_eq_card_quotient_mul_card	1
Total	1

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq_card_quotient_mul_card 📖	mathematical	—	Nat.card Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike HasQuotient.Quotient hasQuotient	—	mul_comm Nat.card_prod Nat.card_congr

---

← Back to Index