Cardinality

📁 Source: Mathlib/LinearAlgebra/Projectivization/Cardinality.lean

Statistics

Metric	Count
Definitions equivQuotientOrbitRel, nonZeroEquivProjectivizationProdUnits	2
Theorems card, card', card'', card_of_finrank, card_of_finrank_two, finite_iff_of_finite, finite_of_finite, isEmpty_of_subsingleton	8
Total	10

Projectivization

Definitions

Name	Category	Theorems
equivQuotientOrbitRel 📖	CompOp	—
nonZeroEquivProjectivizationProdUnits 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Nat.card Projectivization	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Nat.card_unique Zero.instNonempty tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Nat.card_of_isEmpty isEmpty_of_subsingleton MulZeroClass.zero_mul finite_or_infinite Fintype.card_subtype_compl Fintype.card_unique finite_of_finite Fintype.card_units Fintype.card_congr Fintype.card_prod not_iff_not finite_iff_of_finite Nat.card_eq_zero_of_infinite zero_tsub Module.Free.infinite Module.Free.of_divisionRing MulZeroClass.mul_zero
card' 📖	mathematical	—	Nat.card Projectivization	—	card Nat.card_pos Zero.instNonempty
card'' 📖	mathematical	—	Nat.card Projectivization Field.toDivisionRing	—	Finite.one_lt_card EuclideanDomain.toNontrivial card
card_of_finrank 📖	mathematical	Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Nat.card Projectivization Field.toDivisionRing Finset.sum Nat.instAddCommMonoid Finset.range Monoid.toNatPow Nat.instMonoid	—	Finite.one_lt_card EuclideanDomain.toNontrivial RingHomInvPair.ids IsNoetherianRing.strongRankCondition PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain Module.Free.of_divisionRing Module.Free.function Finite.of_fintype Module.Free.self Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite isNoetherian_of_finite FiniteDimensional.finiteDimensional_pi' FiniteDimensional.finiteDimensional_self Module.finrank_fintype_fun_eq_card Fintype.card_fin Nat.card_congr Nat.card_fun Nat.card_eq_fintype_card Nat.cast_mul Nat.cast_sum Finset.sum_congr Nat.cast_pow LT.lt.le geom_sum_mul card Nat.cast_pred LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass Nontrivial.to_nonempty Mathlib.Tactic.Contrapose.contrapose₂ finite_iff_of_finite Module.finrank_of_not_finite Mathlib.Tactic.Contrapose.contrapose₄ Module.finite_of_finite Nat.card_eq_zero_of_infinite
card_of_finrank_two 📖	mathematical	Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Nat.card Projectivization Field.toDivisionRing	—	card_of_finrank geom_sum_two
finite_iff_of_finite 📖	mathematical	—	Finite Projectivization	—	Finite.of_equiv Finite.instProd instFiniteUnits Subtype.coe_eta Finite.instSum Finite.of_fintype finite_of_finite
finite_of_finite 📖	mathematical	—	Finite Projectivization	—	Finite.of_equiv Subtype.finite Finite.prod_left
isEmpty_of_subsingleton 📖	mathematical	—	IsEmpty Projectivization	—	Equiv.isEmpty

---

← Back to Index