Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-27 17:47 ec51fb79

View on Github →

chore(algebra/order/floor): prove subsingletons (#9996)

Estimated changes

Modified src/algebra/continued_fractions/computation/terminates_iff_rat.lean

Modified src/algebra/order/floor.lean

deleted theorem floor_ring_unique

deleted theorem floor_semiring_unique

added theorem subsingleton_floor_ring

added theorem subsingleton_floor_semiring