mk_eq_mk' — Mathlib

English

mk'_eq_zero' states mk' f m s = 0 iff there exists s' ∈ S with s'•m = 0.

Русский

mk'_eq_zero' гласит: mk' f m s = 0 тогда и только тогда, когда существует s' ∈ S с s'•m = 0.

LaTeX

$$$mk' f m s = 0 \\iff \\exists s' \\in S, s' \\cdot m = 0$$$

Lean4

theorem mk_eq_mk' (s : S) (m : M) : LocalizedModule.mk m s = mk' (LocalizedModule.mkLinearMap S M) m s := by
  rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_apply]

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