liftEquiv_id — Mathlib

English

Let p be a natural number. If the base map is the identity RingHom, then the lifting equivalence is the identity equivalence.

Русский

Пусть p — натуральное число. Если отображение основания тождественно, то эквивалент подъёма является тождественной эквивалентностью.

LaTeX

$$$ \operatorname{liftEquiv}(M, \mathrm{RingHom.id}\,K, p) = \mathrm{Equiv.refl}(M) $$$

Lean4

@[simp]
theorem liftEquiv_id : liftEquiv M (RingHom.id K) p = Equiv.refl _ :=
  Equiv.ext (liftEquiv_id_apply · p)

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