mapAlgEquiv_id — Mathlib

English

The mapAlgEquiv construction is functorial with respect to identity: mapAlgEquiv of the identity algebra equivalence is the identity map.

Русский

Конструкция mapAlgEquiv сохраняет тождественный изоморфизм: mapAlgEquiv для тождестенного алгебраического эквивалента дают тождественный изоморфизм.

LaTeX

$$$$\mathrm{Polynomial.mapAlgEquiv}(\mathrm{AlgEquiv.refl}) = \mathrm{AlgEquiv.refl}.$$$$

Lean4

@[simp]
theorem mapAlgEquiv_id : mapAlgEquiv (@AlgEquiv.refl R A _ _ _) = AlgEquiv.refl :=
  AlgEquiv.ext fun _x => map_id

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