sec_spec' — Mathlib

English

Let z ∈ S with sec M z = (x, y). Then algebraMap R S x = algebraMap R S (IsLocalization.sec M z).2 ⋅ z, i.e., f(x) = f(y)·z.

Русский

Пусть z ∈ S и sec M z = (x, y). Тогда f(x) = f(y)·z, где f = algebraMap R S.

LaTeX

$$$ \\varphi(x) = \\varphi(y)\\, z \\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 just an application of `S`'s commutativity. -/
theorem sec_spec' (z : S) : algebraMap R S (IsLocalization.sec M z).1 = algebraMap R S (IsLocalization.sec M z).2 * z :=
  by rw [mul_comm, sec_spec]

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