mul_div_cancel' — Mathlib

English

If b ≠ 0 and b ∣ a, then b · (a / b) = a; a generalization of the Int.div_one note.

Русский

Если b ≠ 0 и b делит a, то b · (a / b) = a; обобщение примечания Int.div_one.

LaTeX

$$$ b \neq 0 \land b \mid a \Rightarrow b * (a / b) = a $$$

Lean4

protected theorem mul_div_cancel' {a b : R} (hb : b ≠ 0) (hab : b ∣ a) : b * (a / b) = a := by
  rw [← mul_div_assoc _ hab, mul_div_cancel_left₀ _ hb]
    -- This generalizes `Int.div_one`, see note [simp-normal form]

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