sq_pos_of_pos — Mathlib

English

Let M be a monoid with zero and a partial order such that multiplying by a positive element preserves order. Then if a > 0, we have a^2 > 0.

Русский

Пусть M – моноид с нулём и частичным порядком, при этом умножение на положительный элемент строго сохраняет порядок. Тогда если a > 0, то a^2 > 0.

LaTeX

$$$0 < a \Rightarrow 0 < a^2$$$

Lean4

theorem sq_pos_of_pos [PosMulStrictMono M₀] (ha : 0 < a) : 0 < a ^ 2 := by simpa only [sq] using mul_pos ha ha

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