prod_le — Mathlib

English

For nontrivial α, a.prod ≤ b.prod iff a ≤ b.

Русский

Для ненулевого α, a.prod ≤ b.prod тогда и только если a ≤ b.

LaTeX

$$prod_le [Nontrivial α] {a b : FactorSet α} : a.prod ≤ b.prod ↔ a ≤ b$$

Lean4

theorem prod_le [Nontrivial α] {a b : FactorSet α} : a.prod ≤ b.prod ↔ a ≤ b :=
  by
  refine ⟨fun h ↦ ?_, prod_mono⟩
  have : a.prod.factors ≤ b.prod.factors := factors_mono h
  rwa [prod_factors, prod_factors] at this

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