charZero — Mathlib

English

If α has CharZero, then WithTop α also has CharZero; the injection Nat.cast from α to WithTop α is compatible with the nat cast in α.

Русский

Если у α есть CharZero, то и WithTop α имеет CharZero; вложение Nat.cast совместимо с nat cast в α.

LaTeX

$$$\\\\instance\\\n CharZero (WithTop α) \\\\text{ когда } [AddMonoidWithOne α] [CharZero α]$$$

Lean4

instance charZero [AddMonoidWithOne α] [CharZero α] : CharZero (WithTop α) :=
  {
    cast_injective :=
      Function.Injective.comp (f := Nat.cast (R := α)) (fun _ _ => WithTop.coe_eq_coe.1) Nat.cast_injective }

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