mk'_sub_mk' — Mathlib

English

Product of two mk' elements equals mk' of product under multiplicativity of f.

Русский

Произведение двух mk' элементов равно mk' от произведения при мультипликативности f.

LaTeX

$$$(mk' f m_1 s_1)\\cdot (mk' f m_2 s_2) = mk' f (m_1 m_2) (s_1 s_2)$$$

Lean4

theorem mk'_sub_mk' {M M' : Type*} [AddCommGroup M] [SubtractionCommMonoid M'] [Module R M] [Module R M']
    (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ m₂ : M) (s₁ s₂ : S) :
    mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂) := by
  rw [sub_eq_add_neg, ← mk'_neg, mk'_add_mk', smul_neg, ← sub_eq_add_neg]

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