English
Let z ∈ S and write sec M z = (x, y) ∈ R × M. Then z multiplied by the image of y equals the image of x: z·f(y) = f(x), where f = algebraMap R S.
Русский
Пусть z ∈ S и запись sec M z = (x, y) ∈ R × M. Тогда z, умноженное на образ y в S, равно образу x: z·f(y) = f(x), где f = алгебраическое отображение от R в S.
LaTeX
$$$ z\\,\\varphi(y) = \\varphi(x) \\quad\\text{where } (x,y) = \\operatorname{sec}_M(z), \\; \\varphi = \\text{algebraMap } R S $$$
Lean4
/-- Given `z : S`, `IsLocalization.sec M z` is defined to be a pair `(x, y) : R × M` such
that `z * f y = f x` (so this lemma is true by definition). -/
theorem sec_spec (z : S) : z * algebraMap R S (IsLocalization.sec M z).2 = algebraMap R S (IsLocalization.sec M z).1 :=
Classical.choose_spec <| IsLocalization.surj _ z
