mk'_self' — Mathlib

English

In the localization of M at the submonoid S, for every y in S, the image of the pair (y, y) equals the multiplicative identity 1; i.e., y/y = 1 in the localized monoid S^{-1}M.

Русский

В локализации M по подсополом S для каждого элемента y∈S образ пары (y, y) равен единице; то есть y/y = 1 в локализации S^{-1}M.

LaTeX

$$$\\forall y \\in S:\\; \\text{mk}'(y, y) = 1$ in the localization S^{-1}M (i.e. the fraction $y/y$ equals 1).$$

Lean4

@[to_additive (attr := simp)]
theorem mk'_self' (y : S) : f.mk' (y : M) y = 1 :=
  show _ * _ = _ by rw [mul_inv_left, mul_one]; dsimp

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