toCharZero — Mathlib

English

There is a CharZero structure on any AddMonoidWithOne R, compatible with the existing order structure.

Русский

Существует структура CharZero на любом AddMonoidWithOne R, совместимая с существующим порядком.

LaTeX

$$$ \\forall R [AddMonoidWithOne R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R],\\; \\text{CharZero } R. $$$

Lean4

/-- This is not an instance, as it would loop with `NeZero.charZero_one`. -/
theorem toCharZero {R} [AddMonoidWithOne R] [PartialOrder R] [ZeroLEOneClass R] [NeZero (1 : R)] [AddLeftStrictMono R] :
    CharZero R where
  cast_injective := (strictMono_nat_of_lt_succ fun n ↦ by rw [Nat.cast_succ]; apply lt_add_one).injective

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