semiring — Mathlib

English

There is a subtraction operation on the nonnegative subtype defined by restricting difference via nonnegification: Sub x y is defined as toNonneg(x − y).

Русский

На подтипе неотрицательных элементов существует операция вычитания, заданная как toNonneg(x − y).

LaTeX

$$$ [Sub \alpha] \Rightarrow Sub \{ x : \alpha // 0 \le x \} : Sub (Subtype fun x => 0 \le x) $$$

Lean4

instance semiring : Semiring { x : α // 0 ≤ x } :=
  Subtype.coe_injective.semiring _ Nonneg.coe_zero Nonneg.coe_one (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ => rfl

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