semifield — Mathlib

English

The nonnegative part of a semifield inherits a semifield structure with the inherited operations.

Русский

Неотрицательная часть полуполевая сохраняет структуру полуполе, с унаследованными операциями.

LaTeX

$$$\\text{Nonneg}(\\alpha)$ имеет структуру semifield с теми же операциями, ограниченными на неотрицательные элементы.$$

Lean4

instance semifield : Semifield { x : α // 0 ≤ x } :=
  fast_instance%Subtype.coe_injective.semifield _ Nonneg.coe_zero Nonneg.coe_one Nonneg.coe_add Nonneg.coe_mul
      Nonneg.coe_inv Nonneg.coe_div (fun _ _ => rfl) coe_nnqsmul Nonneg.coe_pow Nonneg.coe_zpow Nonneg.coe_natCast
      coe_nnratCast

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