Theorems · Theorem · order theory

CeilDiv.ceilDiv_gc

∀ {α : Type u_2} {β : Type u_3} {inst : AddCommMonoid α} {inst_1 : PartialOrder α} {inst_2 : AddCommMonoid β}
  {inst_3 : PartialOrder β} {inst_4 : SMulZeroClass α β} [self : CeilDiv α β] ⦃a : α⦄,
  0 < a → GaloisConnection (fun x => x ⌈/⌉ a) fun x => a • x

Do not use this. Use gc_smul_ceilDiv or gc_mul_ceilDiv instead.

Defined in

Mathlib.Algebra.Order.Floor.Div

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

CeilDiv