withOneCongr

Mathlib.Algebra.Group.WithOne.Basic

URI: https://scilib.ai/kg/mathlib#MulEquiv.withOneCongr

Lean4

/-- A version of `Equiv.optionCongr` for `WithOne`. -/
@[to_additive (attr := simps apply) /-- A version of `Equiv.optionCongr` for `WithZero`. -/
    ]
def _root_.MulEquiv.withOneCongr (e : α ≃* β) : WithOne α ≃* WithOne β :=
  { mapMulHom e.toMulHom with
    toFun := mapMulHom e.toMulHom, invFun := mapMulHom e.symm.toMulHom, left_inv := (by induction · <;> simp)
    right_inv := (by induction · <;> simp) }

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

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

Разделы

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

Аффилиация

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