instMulPosStrictMono — Mathlib

English

If α has NoZeroDivisors, then WithBot α has NoZeroDivisors. The property is inherited by the bottom-extended structure.

Русский

Если у α нет нулевых делителей, то и WithBot α не имеет нулевых делителей. Свойство наследуется.

LaTeX

$$$\text{NoZeroDivisors}(α) \Rightarrow \text{NoZeroDivisors}(WithBot α)$$$

Lean4

instance [MulZeroClass α] [Preorder α] [MulPosStrictMono α] : MulPosStrictMono (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only
    lift x to α using x0.ne_bot
    cases b
    · exact absurd h not_lt_bot
    cases a
    · simp_rw [bot_mul x0.ne.symm, ← coe_mul, bot_lt_coe]
    simp only [← coe_mul, coe_lt_coe] at *
    norm_cast at x0
    exact mul_lt_mul_of_pos_right h x0

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