sub_mk — Mathlib

English

The mk' operation preserves subtraction in Localization: mk' S (x1*y2 − x2*y1) (y1*y2) = mk' S x1 y1 − mk' S x2 y2.

Русский

Операция mk' сохраняет вычитание в локализации: mk' S (x1*y2 − x2*y1) (y1*y2) = mk' S x1 y1 − mk' S x2 y2.

LaTeX

$$$\\mathrm{mk'}\\ S (x_1 y_2 - x_2 y_1) (y_1 y_2) = \\mathrm{mk'}\\ S x_1 y_1 - \\mathrm{mk'}\\ S x_2 y_2$$$

Lean4

theorem sub_mk (a c) (b d) : (mk a b : Localization M) - mk c d = mk ((d : R) * a - b * c) (b * d) := by
  rw [sub_eq_add_neg, neg_mk, add_mk, add_comm, mul_neg, ← sub_eq_add_neg]

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