mapEquiv_refl — Mathlib

English

The map induced by the identity algebra equivalence is the identity on mv-polynomials.

Русский

Отображение, порожденное тождественным алгебраическим эквивалентом, является тождественным отображением на MV-многочленах.

LaTeX

$$$$ mapAlgEquiv \\; σ\\; (AlgEquiv.refl) = AlgEquiv.refl. $$$$

Lean4

@[simp]
theorem mapEquiv_refl : mapEquiv σ (RingEquiv.refl R) = RingEquiv.refl _ :=
  RingEquiv.ext map_id

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