toBasicOpen_mk' — Mathlib

English

The action of toBasicOpen on a fraction mk' matches the corresponding constant section on a basic open.

Русский

Применение toBasicOpen к дроби mk' совпадает с соответствующей константной секцией на базовом открытом.

LaTeX

$$$toBasicOpen(R,f) (IsLocalization.mk'(Localization.Away f, a, b)) = const(R, a, f, \\operatorname{basicOpen} f) \\; \\text{up to the usual identifications}.$$$

Lean4

@[simp]
theorem toBasicOpen_mk' (s f : R) (g : Submonoid.powers s) :
    toBasicOpen R s (IsLocalization.mk' (Localization.Away s) f g) =
      const R f g (PrimeSpectrum.basicOpen s) fun _ hx => Submonoid.powers_le.2 hx g.2 :=
  (IsLocalization.lift_mk'_spec _ _ _ _).2 <| by rw [toOpen_eq_const, toOpen_eq_const, const_mul_cancel']

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