mk'_cancel_right — Mathlib

English

Two fractions mk' f m1 s1 and mk' f m2 s2 are equal iff there exists s ∈ S with s·s1·m2 = s·s2·m1.

Русский

Две дроби mk' f m1 s1 и mk' f m2 s2 равны тогда и только тогда, когда существует s ∈ S такое, что s·s1·m2 = s·s2·m1.

LaTeX

$$$mk' f m_1 s_1 = mk' f m_2 s_2 \\iff \\exists s \\in S, \\ s \\cdot s_1 \\cdot m_2 = s \\cdot s_2 \\cdot m_1$$$

Lean4

@[simp]
theorem mk'_cancel_right (m : M) (s₁ s₂ : S) : mk' f (s₂ • m) (s₁ * s₂) = mk' f m s₁ :=
  by
  delta mk'
  rw [LocalizedModule.mk_cancel_common_right]

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