Theorems · Theorem · geometry

Projectivization.card_of_finrank

∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k] {n : ℕ},
  Module.finrank k V = n → Nat.card (Projectivization k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Defined in

Mathlib.LinearAlgebra.Projectivization.Cardinality

Cited by

1 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldAddCommGroupModuleFinite