Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-15 02:10 53b216bc

View on Github →

refactor(algebra/order/ring): Make strict_ordered_semirings nontrivial (#17394) strict_ordered_semiring + nontrivial implies char_zero, but this can't be instance because char_zero implies nontrivial Instead of waiting for Lean 4, where such looping instances are possible, we make all strict_ordered_semirings nontrivial, because we don't care about types with one element beingstrict_ordered_semirings.

Estimated changes

modified theorem geom_sum_pos
modified theorem exists_nat_gt
deleted theorem nat.strict_mono_cast
modified theorem list.prod_pos
modified theorem nat.cast_le
modified theorem nat.cast_le_one
modified theorem nat.cast_lt
modified theorem nat.cast_lt_one
modified theorem nat.one_le_cast
modified theorem nat.one_lt_cast
added theorem nat.strict_mono_cast
modified theorem int.comap_coe_at_bot
modified theorem int.comap_coe_at_top
modified theorem nat.comap_coe_at_top
modified theorem tendsto_coe_int_at_bot_iff
modified theorem tendsto_coe_int_at_top_iff
modified theorem tendsto_coe_nat_at_top_iff
modified theorem mem_pos_monoid
modified def pos_submonoid