instCharZero — Mathlib

English

Cardinal numbers form a characteristic-zero semiring; the natural embedding of natural numbers into cardinals is injective.

Русский

Кардинальные числа образуют полугруппу с нулём, характерную нулю; естественная инъекция натуральных чисел в кардиналы инъективна.

LaTeX

$$CharZero( Cardinal )$$

Lean4

instance : CharZero Cardinal := by
  refine ⟨fun a b h ↦ ?_⟩
  rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq, Fintype.card_fin, Fintype.card_fin] at h

Похожие утверждения