factorizationLCMRight_pos — Mathlib

English

The right factorization of the LCM is also strictly positive.

Русский

Правая факторизация НОК также положительна.

LaTeX

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

Lean4

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

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