involutiveInv

Mathlib.Algebra.Group.InjSurj

URI: https://scilib.ai/kg/mathlib#Function.Surjective.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 : Surjective f)
    (inv : ∀ x, f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₂
    where
  inv := Inv.inv
  inv_inv := hf.forall.2 fun x => by rw [← inv, ← inv, inv_inv]

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

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

Разделы

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

Аффилиация

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