Projectivization.card
∀ (k : Type u_1) (V : Type u_2) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V], Nat.card V - 1 = Nat.card (Projectivization k V) * (Nat.card k - 1)
Fraction free cardinality formula for the points of ℙ k V if k and V are finite
(for silly reasons the formula also holds when k and V are infinite).
See Projectivization.card' and Projectivization.card'' for other spellings of the formula.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites29
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Fintypeproof · cited by 7,736
- Finiteproof · cited by 3,029
- Unitsproof · cited by 2,804
- Nontrivialproof · cited by 2,416
- MulZeroClass.mul_zeroproof · cited by 2,091
- MulZeroClass.zero_mulproof · cited by 1,625
- Fintype.cardproof · cited by 1,386
- DivisionRingstatement and proof · cited by 1,062
- Nat.cardstatement and proof · cited by 844
- Infiniteproof · cited by 352
Cited by3
Results whose statement or proof uses this declaration.
- Projectivization.card_of_finrankproof · cited by 1
- Projectivization.card'proof · cited by 0
- Projectivization.card''proof · cited by 0