mk'_mk_eq_div — Mathlib

English

The localization constructor mk' corresponds to the division operation in the target ring: mk' r ⟨s, hs⟩ equals algebraMap(r)/algebraMap(s).

Русский

Конструктор локализации mk' соответствует делению в целевом кольце: mk' r ⟨s, hs⟩ = algebraMap(r)/algebraMap(s).

LaTeX

$$mk'_mk_eq_div {r} (s : nonZeroDivisors A) : mk' K r ⟨s, hs⟩ = algebraMap A K r / algebraMap A K s$$

Lean4

theorem mk'_mk_eq_div {r s} (hs : s ∈ nonZeroDivisors A) : mk' K r ⟨s, hs⟩ = algebraMap A K r / algebraMap A K s :=
  haveI := (algebraMap A K).domain_nontrivial
  mk'_eq_iff_eq_mul.2 <|
    (div_mul_cancel₀ (algebraMap A K r) (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hs)).symm

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