Theorems · Theorem · order theory

Nat.floor_congr

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {S : Type u_3}
  [inst_3 : Semiring S] [inst_4 : LinearOrder S] [inst_5 : FloorSemiring S] {b : S} [IsStrictOrderedRing R]
  [IsStrictOrderedRing S], (∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b) → ⌊a⌋₊ = ⌊b⌋₊

Defined in

Mathlib.Algebra.Order.Floor.Semiring

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringLinearOrderFloorSemiringSemiringLinearOrderFloorSemiringIsStrictOrderedRingIsStrictOrderedRing