instMulLeftMono — Mathlib

English

0 is strictly less than any nonzero coerced element in WithZero α.

Русский

0 строго меньше любого ненулевого элемента в WithZero α, приведённого из α.

LaTeX

$$$ 0 < (a : \mathrm{WithZero} \alpha) $$$

Lean4

instance instMulLeftMono [Mul α] [MulLeftMono α] : MulLeftMono (WithZero α) :=
  by
  refine ⟨fun a b c hbc => ?_⟩
  induction a; · exact zero_le _
  induction b; · exact zero_le _
  rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
  rw [← coe_mul _ c, ← coe_mul, coe_le_coe]
  exact mul_le_mul_left' hbc' _

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