Mathlib Map

Theorems · Theorem · order theory

Int.cast_strictMono

∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1],
  StrictMono fun x => ↑x
Defined in
Mathlib.Algebra.Order.Ring.Cast
Cited by
1 results in Mathlib
Foundations
Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommGroupWithOnePartialOrderAddLeftMonoZeroLEOneClassNeZero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Int.cast_lt · cited by 14Int.cast_ltPartialOrder · cited by 6410PartialOrderStrictMono · cited by 706StrictMonoAddLeftMono · cited by 687AddLeftMonoZeroLEOneClass · cited by 304ZeroLEOneClassAddCommGroupWithOne · cited by 61AddCommGroupWithOneInt.cast_le · cited by 28Int.cast_lestrictMono_of_le_iff_le · cited by 14strictMono_of_le_iff_leInt.cast_strictMonoCITED BYCITES

Cites7

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.