nat_lcm_helper

Mathlib.Tactic.NormNum.GCD

URI: https://scilib.ai/kg/mathlib#Tactic.NormNum.nat_lcm_helper

Lean4

theorem nat_lcm_helper (x y d m : ℕ) (hd : Nat.gcd x y = d) (d0 : Nat.beq d 0 = false) (dm : x * y = d * m) :
    Nat.lcm x y = m :=
  mul_right_injective₀ (Nat.ne_of_beq_eq_false d0) <| by
    dsimp only
    rw [← dm, ← hd, Nat.gcd_mul_lcm]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru