invOneClass

Mathlib.Algebra.Group.InjSurj

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

Lean4

/-- A type endowed with `1` and `⁻¹` is a `InvOneClass`, if it admits an injective map that
preserves `1` and `⁻¹` to a `InvOneClass`.  See note [reducible non-instances]. -/
@[to_additive /-- A type endowed with `0` and unary `-` is an `NegZeroClass`, if it admits an
    injective map that preserves `0` and unary `-` to an `NegZeroClass`. -/
    ]
protected abbrev invOneClass [InvOneClass M₂] (f : M₁ → M₂) (hf : Injective f) (one : f 1 = 1)
    (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) : InvOneClass M₁ :=
  { ‹One M₁›, ‹Inv M₁› with inv_one := hf <| by rw [inv, one, inv_one] }

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

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

Разделы

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

Аффилиация

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