mk'_sub — Mathlib

English

In IsLocalization, mk'_sub expresses that mk' preserves subtraction: IsLocalization.mk'_sub expresses the subtraction identity in the localized ring.

Русский

В IsLocalization mk'_sub выражает сохранение вычитания: идентичность вычитания в локализованной структуре.

LaTeX

$$$\\text{IsLocalization.mk'_sub}\\ S x_1 x_2 y_1 y_2 = \\text{...}$$$

Lean4

theorem mk'_sub (x₁ x₂ : R) (y₁ y₂ : M) : mk' S (x₁ * y₂ - x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂ := by
  rw [sub_eq_add_neg, sub_eq_add_neg, ← mk'_neg, ← mk'_add, neg_mul]

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