Theorems · Theorem · order theory

tsub_div

∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [IsStrictOrderedRing α]
  [inst_4 : Sub α] [OrderedSub α] (a b c : α), (a - b) / c = a / c - b / c

Defined in

Mathlib.Algebra.Order.Field.Canonical

Cited by

2 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemifieldLinearOrderCanonicallyOrderedAddIsStrictOrderedRingSubOrderedSub