toMulEquiv_symm

Mathlib.Algebra.Star.MonoidHom

URI: https://scilib.ai/kg/mathlib#StarMulEquiv.toMulEquiv_symm

Lean4

@[simp]
theorem toMulEquiv_symm (f : A ≃⋆* B) : f.symm.toMulEquiv = f.toMulEquiv.symm :=
  rfl

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

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

Разделы

Аффилиация

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