Theorems · Theorem · number theory

round_sub_intCast

∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α)
  (y : ℤ), round (x - ↑y) = round x - y

Defined in

Mathlib.Algebra.Order.Round

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingLinearOrderIsStrictOrderedRingFloorRing