mapEquiv_refl

Mathlib.Algebra.Star.Unitary

URI: https://scilib.ai/kg/mathlib#unitary.mapEquiv_refl

English

The mapEquiv for the refl isomorphism is the refl isomorphism on unitary substructures.

Русский

MapEquiv для отражения тождественности есть тождественный изоморфизм на единицах.

LaTeX

$$$ mapEquiv(\\mathrm{refl}\\ R) = \\mathrm{refl}(\\mathrm{unitary} R)$$$

Lean4

@[simp]
theorem mapEquiv_refl : mapEquiv (.refl R) = .refl (unitary R) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru