mk'_spec — Mathlib

English

Let f be a localization map of S in M to N. For every x in M and y in S, the element f.mk'(x, y) in N satisfies f.mk'(x, y) · f(y) = f(x).

Русский

Пусть f — отображение локализации S в M в N. Для любых x ∈ M и y ∈ S выполняется f.mk'(x, y) · f(y) = f(x).

LaTeX

$$$f.mk'(x,y)\\;f(y) = f(x)$$$

Lean4

@[to_additive]
theorem mk'_spec (x) (y : S) : f.mk' x y * f y = f x :=
  show _ * _ * _ = _ by rw [mul_assoc, mul_comm _ (f y), ← mul_assoc, mul_inv_left, mul_comm]; dsimp

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