Documentation

ClassFieldTheory.Mathlib.SetTheory.Cardinal.Finite

source
@[simp]
theorem Nat.card_ne_zero' {α : Type u_1} [Nonempty α] [Finite α] :
Nat.card α ≠ 0