Mathlib Map

Theorems · Theorem · order theory

MulPosMono.toMulPosStrictMono

∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : PartialOrder α] [IsRightCancelMulZero α] [MulPosMono α],
  MulPosStrictMono α
Defined in
Mathlib.Algebra.Order.GroupWithZero.Basic
Cited by
1 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
MonoidWithZeroPartialOrderIsRightCancelMulZeroMulPosMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

mulPosMono_iff_mulPosStrictMono · cited by 0mulPosMono_iff_mulPosStri…PartialOrder · cited by 6410PartialOrderLT.lt.le · cited by 2189lt.leLT.lt.ne' · cited by 1417lt.ne'LT.lt.ne · cited by 872lt.neMonoidWithZero · cited by 456MonoidWithZeromul_le_mul_of_nonneg_right · cited by 301mul_le_mul_of_nonneg_rightMulPosMono · cited by 128MulPosMonoLE.le.lt_of_ne · cited by 116le.lt_of_neMulPosStrictMono · cited by 94MulPosStrictMonoIsRightCancelMulZero · cited by 33IsRightCancelMulZeromul_right_cancel₀ · cited by 22mul_right_cancel₀MulPosMono.toMulPosStrictMonoCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.