Theorems · Definition · order theory

CeilDiv.casesOn

{α : Type u_2} →
  {β : Type u_3} →
    [inst : AddCommMonoid α] →
      [inst_1 : PartialOrder α] →
        [inst_2 : AddCommMonoid β] →
          [inst_3 : PartialOrder β] →
            [inst_4 : SMulZeroClass α β] →
              {motive : CeilDiv α β → Sort u} →
                (t : CeilDiv α β) →
                  ((ceilDiv : β → α → β) →
                      (ceilDiv_gc : ∀ ⦃a : α⦄, 0 < a → GaloisConnection (fun x => ceilDiv x a) fun x => a • x) →
                        (ceilDiv_nonpos : ∀ ⦃a : α⦄, a ≤ 0 → ∀ (b : β), ceilDiv b a = 0) →
                          (zero_ceilDiv : ∀ (a : α), ceilDiv 0 a = 0) →
                            motive
                              { ceilDiv := ceilDiv, ceilDiv_gc := ceilDiv_gc, ceilDiv_nonpos := ceilDiv_nonpos,
                                zero_ceilDiv := zero_ceilDiv }) →
                    motive t

Defined in

Mathlib.Algebra.Order.Floor.Div

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

AddCommMonoidPartialOrderAddCommMonoidPartialOrderSMulZeroClass