involutiveInv

Mathlib.Algebra.Group.InjSurj

URI: https://scilib.ai/kg/mathlib#Function.Injective.involutiveInv

Lean4

/-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type
which has an involutive inversion. See note [reducible non-instances] -/
@[to_additive /-- A type has an involutive negation if it admits a surjective map that
    preserves `-` to a type which has an involutive negation. -/
    ]
protected abbrev involutiveInv {M₁ : Type*} [Inv M₁] [InvolutiveInv M₂] (f : M₁ → M₂) (hf : Injective f)
    (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₁
    where
  inv := Inv.inv
  inv_inv x := hf <| by rw [inv, inv, inv_inv]

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

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

Разделы

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

Аффилиация

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