neg_mk — Mathlib

English

There exists a negation operation on PerfectClosure K p defined via lifting negation from the product K and the natural numbers through the Quot construction, compatible with the Frobenius structure.

Русский

Существует операция отрицания на PerfectClosure K p, заданная через отображение отрицания из произведения K × ℕ и факторизации через Quot, совместимая с Frobenius.

LaTeX

$$Neg (PerfectClosure K p)$$

Lean4

@[simp]
theorem neg_mk (x : ℕ × K) : -mk K p x = mk K p (x.1, -x.2) :=
  rfl

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