instExistsMulOfLE — Mathlib

English

For α × β, if a ≤ b, then there exists c with b = a · c (componentwise).

Русский

Для произведения α × β: если a ≤ b, то существует c such that b = a · c (покомпонентно).

LaTeX

$$ExistsMulOfLE(α × β)$$

Lean4

@[to_additive]
instance [LE α] [LE β] [Mul α] [Mul β] [ExistsMulOfLE α] [ExistsMulOfLE β] : ExistsMulOfLE (α × β) :=
  ⟨fun h =>
    let ⟨c, hc⟩ := exists_mul_of_le h.1
    let ⟨d, hd⟩ := exists_mul_of_le h.2
    ⟨(c, d), Prod.ext hc hd⟩⟩

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