numeratorUnit — Mathlib

English

For s ∈ S, the fraction s/1 represents a unit in the localization R[S⁻¹], i.e., s/1 is invertible with inverse 1/s.

Русский

Для s ∈ S дробь s/1 представляет единицу в локализации R[S⁻¹], то есть s/1 обратимо и имеет обратную 1/s.

LaTeX

$$$(s / 1) \\in (R[S^{-1}])^\\times,$ with inverse $(1 / s)$.$$

Lean4

/-- The fraction `s /ₒ 1` as a unit in `R[S⁻¹]`, where `s : S`. -/
@[to_additive /-- The difference `s -ₒ 0` as a an additive unit. -/
    ]
def numeratorUnit (s : S) : Units R[S⁻¹] where
  val := (s : R) /ₒ 1
  inv := (1 : R) /ₒ s
  val_inv := OreLocalization.mul_inv s 1
  inv_val := OreLocalization.mul_inv 1 s

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