surj'' — Mathlib

English

Every element z in S can be written as r · (1/m) for some r ∈ R and m ∈ M via the embedding, i.e., z = r · (toInvSubmonoid M S m : S).

Русский

Каждый элемент z в S можно записать как z = r · (1/m) для некоторого r из R и m из M через отображение, то есть z = r · (toInvSubmonoid M S m).

LaTeX

$$$\exists r\in R,\exists m\in M, z = r \cdot (toInvSubmonoid M S m : S)$$$

Lean4

theorem surj'' (z : S) : ∃ (r : R) (m : M), z = r • (toInvSubmonoid M S m : S) :=
  by
  rcases IsLocalization.surj M z with ⟨⟨r, m⟩, e : z * _ = algebraMap R S r⟩
  refine ⟨r, m, ?_⟩
  rw [Algebra.smul_def, ← e, mul_assoc]
  simp

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