trans

Mathlib.Algebra.Star.MonoidHom

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

Lean4

/-- Transitivity of `StarMulEquiv`. -/
@[trans]
def trans (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C) : A ≃⋆* C :=
  { e₁.toMulEquiv.trans e₂.toMulEquiv with
    map_star' := fun a =>
      show e₂.toFun (e₁.toFun (star a)) = star (e₂.toFun (e₁.toFun a)) by rw [e₁.map_star', e₂.map_star'] }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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