mk_eq_mk_iff' — Mathlib

English

Let α be a cancellative commutative monoid and S a submonoid of α. For a1,a2 ∈ α with a2 ∈ S and b1,b2 ∈ S, the elements mk(a1,a2) and mk(b1,b2) are equal in Localization S if and only if b2 · a1 = a2 · b1 in α.

Русский

Пусть α — согласованный коммутативный моноид с отменой, S — подмоноид α. Пусть a1,a2 ∈ α с a2 ∈ S и b1,b2 ∈ S. Тогда mk(a1,a2) = mk(b1,b2) в локализации S тогда и только тогда, когда b2 · a1 = a2 · b1 в α.

LaTeX

$$$\\text{Localization.mk}(a_1,a_2) = \\text{Localization.mk}(b_1,b_2) \\;\\iff\\; b_2 a_1 = a_2 b_1$$$

Lean4

@[to_additive]
theorem mk_eq_mk_iff' : mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = a₂ * b₁ := by
  simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]

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