mapToFractionRing_apply — Mathlib

English

For every b ∈ B, the mapToFractionRing sends b to its lift in the fraction ring via IsLocalization.lift.

Русский

Для каждого $b\\in B$ отображение mapToFractionRing отправляет $b$ в локализацию через IsLocalization.lift.

LaTeX

$$$mapToFractionRing K S B hS(b) = IsLocalization.lift (map_isUnit_of_le K S hS) (b)$$$

Lean4

@[simp]
theorem mapToFractionRing_apply {B : Type*} [CommRing B] [Algebra A B] [IsLocalization S B] (hS : S ≤ A⁰) (b : B) :
    mapToFractionRing K S B hS b = IsLocalization.lift (map_isUnit_of_le K S hS) b :=
  rfl

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