div_eq_iff — Mathlib

English

Let a, b, c ∈ EReal with b ≠ ⊥, b ≠ ⊤, b ≠ 0. Then c / b = a if and only if c = a · b.

Русский

Пусть a, b, c ∈ EReal, b ≠ ⊥, b ≠ ⊤, b ≠ 0. Тогда c / b = a тогда и только тогда, когда c = a · b.

LaTeX

$$$(c / b = a) \iff (c = a b)$$$

Lean4

theorem div_eq_iff (hbot : b ≠ ⊥) (htop : b ≠ ⊤) (hzero : b ≠ 0) : c / b = a ↔ c = a * b :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]
  · rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]

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