instLinearOrderedAddCommGroupWithTopOrderDualAdditive

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#instLinearOrderedAddCommGroupWithTopOrderDualAdditive

Lean4

instance : LinearOrderedAddCommGroupWithTop (Additive α)ᵒᵈ
    where
  neg_top := inv_zero (G₀ := α)
  add_neg_cancel := fun a ha ↦
    mul_inv_cancel₀ (G₀ := α)
      (id ha : a.toMul ≠ 0)
        -- Counterexample with monoid for the backward direction:
        -- Take `Mᵐ⁰` where `M := ℚ ×ₗ ℕ`.

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

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

Разделы

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

Аффилиация

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