lift_id — Mathlib

English

The lift with unit-maps acts as the identity on S, i.e., lift composed with the unit map gives back the original element of S.

Русский

Лифт с отображениями единиц действует как тождественное отображение на S: lift = id на S.

LaTeX

$$$ \\mathrm{lift}\\; (\\mathrm{map\\_units}\\ ; S) = \\mathrm{id}_S. $$$

Lean4

@[simp]
theorem lift_id (x) : lift (map_units S : ∀ _ : M, IsUnit _) x = x :=
  (toLocalizationMap M S).lift_id _

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