Theorems · Theorem · order theory

FloorDiv.floorDiv_nonpos

∀ {α : Type u_2} {β : Type u_3} {inst : AddCommMonoid α} {inst_1 : PartialOrder α} {inst_2 : AddCommMonoid β}
  {inst_3 : PartialOrder β} {inst_4 : SMulZeroClass α β} [self : FloorDiv α β] ⦃a : α⦄, a ≤ 0 → ∀ (b : β), b ⌊/⌋ a = 0

Do not use this. Use floorDiv_nonpos instead.

Defined in

Mathlib.Algebra.Order.Floor.Div

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

FloorDiv