mk'_sub — Mathlib

English

mk' f m s = m' iff f m = s • m' (rephrased form of mk'_eq_iff).

Русский

mk' f m s = m' тогда и только тогда, когда f m = s • m'.

LaTeX

$$$mk' f m s = m' \\iff f m = s \\cdot m'$$$

Lean4

theorem mk'_sub {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) : mk' f (m₁ - m₂) s = mk' f m₁ s - mk' f m₂ s := by
  rw [sub_eq_add_neg, sub_eq_add_neg, mk'_add, mk'_neg]

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