factorizationLCMLeft_pos — Mathlib

English

The left factorization of the LCM is strictly positive for all a,b.

Русский

Левая факторизация НОК положительна для любых a,b.

LaTeX

$$$0 < \text{factorizationLCMLeft}(a,b).$$$

Lean4

theorem factorizationLCMLeft_pos : 0 < factorizationLCMLeft a b :=
  by
  apply Nat.pos_of_ne_zero
  rw [factorizationLCMLeft, Finsupp.prod_ne_zero_iff]
  intro p _ H
  by_cases h : b.factorization p ≤ a.factorization p
  · simp only [h, reduceIte, pow_eq_zero_iff', ne_eq] at H
    simpa [H.1] using H.2
  · simp only [h, reduceIte, one_ne_zero] at H

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