coe_refl — Mathlib

English

The refl of an algebra equivalence maps to the identity ring hom; that is, the underlying map is the identity on the base ring.

Русский

Тождественная эквивалентность отображается в RingHom как тождественный кольцевой гомоморфизм; основание кольца сохраняется.

LaTeX

$$$ refl:\ A_1 \to A_1$ induces $RingHom.id$$$

Lean4

@[simp]
theorem coe_refl : ⇑(refl : A₁ ≃ₐ[R] A₁) = id :=
  rfl

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