numeratorHom — Mathlib

English

There is a canonical multiplicative homomorphism from R to the Ore localization R[S⁻¹], sending r to r/1.

Русский

Существуют канонические гомоморфизмы из R в локализацию Ore, отправляющие r в r/1.

LaTeX

$$$\\text{numeratorHom}: R \\to^* R[S^{-1}],\\; r \\mapsto r/1.$$$

Lean4

/-- The multiplicative homomorphism from `R` to `R[S⁻¹]`, mapping `r : R` to the
fraction `r /ₒ 1`. -/
@[to_additive /-- The additive homomorphism from `R` to `AddOreLocalization R S`,
      mapping `r : R` to the difference `r -ₒ 0`. -/
    ]
def numeratorHom : R →* R[S⁻¹] where
  toFun r := r /ₒ 1
  map_one' := by with_unfolding_all rfl
  map_mul' _ _ := mul_div_one.symm

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