Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-11-06 23:41
f7707875
View on Github →
refactor(*): supremum of several recent refactoring PRs (
#17381
) This is the supremum of
#17376
#17375
#17374
#17362
#17355
#17349
#17347
#17338
#17336
with imports fixed up to accommodate all the overlapping changes to imports.
Estimated changes
Modified
src/algebra/big_operators/order.lean
Modified
src/algebra/euclidean_domain.lean
Modified
src/algebra/gcd_monoid/basic.lean
Modified
src/algebra/group/pi.lean
Modified
src/algebra/group_power/order.lean
Modified
src/algebra/order/field/basic.lean
Modified
src/algebra/order/field/defs.lean
Modified
src/algebra/order/floor.lean
Created
src/algebra/order/group/abs.lean
added
theorem
abs_abs
added
theorem
abs_abs_sub_abs_le_abs_sub
added
theorem
abs_add'
added
theorem
abs_add
added
theorem
abs_add_three
added
theorem
abs_by_cases
added
theorem
abs_choice
added
theorem
abs_eq
added
theorem
abs_eq_abs
added
theorem
abs_eq_max_neg
added
theorem
abs_eq_sup_inv
added
theorem
abs_eq_zero
added
theorem
abs_le'
added
theorem
abs_le
added
theorem
abs_le_abs
added
theorem
abs_le_abs_of_nonneg
added
theorem
abs_le_abs_of_nonpos
added
theorem
abs_le_max_abs_abs
added
theorem
abs_lt
added
theorem
abs_max_le_max_abs_abs
added
theorem
abs_min_le_max_abs_abs
added
theorem
abs_neg
added
theorem
abs_nonneg
added
theorem
abs_nonpos_iff
added
theorem
abs_of_neg
added
theorem
abs_of_nonneg
added
theorem
abs_of_nonpos
added
theorem
abs_of_pos
added
theorem
abs_pos
added
theorem
abs_pos_of_neg
added
theorem
abs_pos_of_pos
added
theorem
abs_sub
added
theorem
abs_sub_abs_le_abs_sub
added
theorem
abs_sub_comm
added
theorem
abs_sub_le
added
theorem
abs_sub_le_iff
added
theorem
abs_sub_lt_iff
added
theorem
abs_zero
added
theorem
add_abs_nonneg
added
theorem
apply_abs_le_mul_of_one_le'
added
theorem
apply_abs_le_mul_of_one_le
added
theorem
dist_bdd_within_interval
added
theorem
eq_of_abs_sub_eq_zero
added
theorem
eq_of_abs_sub_nonpos
added
theorem
eq_or_eq_neg_of_abs_eq
added
theorem
le_abs'
added
theorem
le_abs
added
theorem
le_abs_self
added
theorem
le_of_abs_le
added
theorem
lt_abs
added
theorem
lt_of_abs_lt
added
theorem
max_sub_min_eq_abs'
added
theorem
max_sub_min_eq_abs
added
theorem
min_abs_abs_le_abs_max
added
theorem
min_abs_abs_le_abs_min
added
theorem
neg_abs_le_neg
added
theorem
neg_abs_le_self
added
theorem
neg_le_abs_self
added
theorem
neg_le_of_abs_le
added
theorem
neg_lt_of_abs_lt
added
theorem
sub_le_of_abs_sub_le_left
added
theorem
sub_le_of_abs_sub_le_right
added
theorem
sub_lt_of_abs_sub_lt_left
added
theorem
sub_lt_of_abs_sub_lt_right
Modified
src/algebra/order/group/basic.lean
deleted
theorem
abs_abs
deleted
theorem
abs_abs_sub_abs_le_abs_sub
deleted
theorem
abs_add'
deleted
theorem
abs_add
deleted
theorem
abs_add_three
deleted
theorem
abs_by_cases
deleted
theorem
abs_choice
deleted
theorem
abs_eq
deleted
theorem
abs_eq_abs
deleted
theorem
abs_eq_max_neg
deleted
theorem
abs_eq_sup_inv
deleted
theorem
abs_eq_zero
deleted
theorem
abs_le'
deleted
theorem
abs_le
deleted
theorem
abs_le_abs
deleted
theorem
abs_le_abs_of_nonneg
deleted
theorem
abs_le_abs_of_nonpos
deleted
theorem
abs_le_max_abs_abs
deleted
theorem
abs_lt
deleted
theorem
abs_max_le_max_abs_abs
deleted
theorem
abs_max_sub_max_le_abs
deleted
theorem
abs_max_sub_max_le_max
deleted
theorem
abs_min_le_max_abs_abs
deleted
theorem
abs_min_sub_min_le_max
deleted
theorem
abs_neg
deleted
theorem
abs_nonneg
deleted
theorem
abs_nonpos_iff
deleted
theorem
abs_of_neg
deleted
theorem
abs_of_nonneg
deleted
theorem
abs_of_nonpos
deleted
theorem
abs_of_pos
deleted
theorem
abs_pos
deleted
theorem
abs_pos_of_neg
deleted
theorem
abs_pos_of_pos
deleted
theorem
abs_sub
deleted
theorem
abs_sub_abs_le_abs_sub
deleted
theorem
abs_sub_comm
deleted
theorem
abs_sub_le
deleted
theorem
abs_sub_le_iff
deleted
theorem
abs_sub_lt_iff
deleted
theorem
abs_zero
deleted
theorem
add_abs_nonneg
deleted
theorem
apply_abs_le_mul_of_one_le'
deleted
theorem
apply_abs_le_mul_of_one_le
deleted
theorem
dist_bdd_within_interval
deleted
theorem
eq_of_abs_sub_eq_zero
deleted
theorem
eq_of_abs_sub_nonpos
deleted
theorem
eq_or_eq_neg_of_abs_eq
deleted
theorem
le_abs'
deleted
theorem
le_abs
deleted
theorem
le_abs_self
deleted
theorem
le_iff_forall_lt_one_mul_le
deleted
theorem
le_iff_forall_one_lt_le_mul
deleted
theorem
le_of_abs_le
deleted
theorem
le_of_forall_lt_one_mul_le
deleted
theorem
le_of_forall_one_lt_div_le
deleted
theorem
lt_abs
deleted
theorem
lt_of_abs_lt
deleted
theorem
max_div_div_left'
deleted
theorem
max_div_div_right'
deleted
theorem
max_inv_inv'
deleted
theorem
max_one_div_max_inv_one_eq_self
deleted
theorem
max_sub_max_le_max
deleted
theorem
max_sub_min_eq_abs'
deleted
theorem
max_sub_min_eq_abs
deleted
theorem
min_abs_abs_le_abs_max
deleted
theorem
min_abs_abs_le_abs_min
deleted
theorem
min_div_div_left'
deleted
theorem
min_div_div_right'
deleted
theorem
min_inv_inv'
deleted
theorem
neg_abs_le_neg
deleted
theorem
neg_abs_le_self
deleted
theorem
neg_le_abs_self
deleted
theorem
neg_le_of_abs_le
deleted
theorem
neg_lt_of_abs_lt
deleted
theorem
sub_le_of_abs_sub_le_left
deleted
theorem
sub_le_of_abs_sub_le_right
deleted
theorem
sub_lt_of_abs_sub_lt_left
deleted
theorem
sub_lt_of_abs_sub_lt_right
deleted
theorem
with_top.coe_neg
Created
src/algebra/order/group/bounds.lean
added
theorem
is_glb.exists_between_self_add'
added
theorem
is_glb.exists_between_self_add
added
theorem
is_lub.exists_between_sub_self'
added
theorem
is_lub.exists_between_sub_self
Created
src/algebra/order/group/densely_ordered.lean
added
theorem
le_iff_forall_lt_one_mul_le
added
theorem
le_iff_forall_one_lt_le_mul
added
theorem
le_of_forall_lt_one_mul_le
added
theorem
le_of_forall_one_lt_div_le
Created
src/algebra/order/group/min_max.lean
added
theorem
abs_max_sub_max_le_abs
added
theorem
abs_max_sub_max_le_max
added
theorem
abs_min_sub_min_le_max
added
theorem
max_div_div_left'
added
theorem
max_div_div_right'
added
theorem
max_inv_inv'
added
theorem
max_one_div_max_inv_one_eq_self
added
theorem
max_sub_max_le_max
added
theorem
min_div_div_left'
added
theorem
min_div_div_right'
added
theorem
min_inv_inv'
Created
src/algebra/order/group/prod.lean
Created
src/algebra/order/group/units.lean
Created
src/algebra/order/group/with_top.lean
added
theorem
with_top.coe_neg
Modified
src/algebra/order/hom/ring.lean
Modified
src/algebra/order/invertible.lean
Modified
src/algebra/order/lattice_group.lean
Modified
src/algebra/order/monoid/canonical.lean
Modified
src/algebra/order/nonneg/ring.lean
Modified
src/algebra/order/pi.lean
Modified
src/algebra/order/positive/ring.lean
Created
src/algebra/order/ring/abs.lean
added
theorem
abs_cases
added
theorem
abs_dvd
added
theorem
abs_dvd_abs
added
theorem
abs_dvd_self
added
theorem
abs_eq_iff_mul_self_eq
added
theorem
abs_eq_neg_self
added
theorem
abs_eq_self
added
def
abs_hom
added
theorem
abs_le_iff_mul_self_le
added
theorem
abs_le_one_iff_mul_self_le_one
added
theorem
abs_lt_iff_mul_self_lt
added
theorem
abs_mul
added
theorem
abs_mul_abs_self
added
theorem
abs_mul_self
added
theorem
abs_one
added
theorem
abs_sub_sq
added
theorem
abs_two
added
theorem
dvd_abs
added
theorem
max_zero_add_max_neg_zero_eq_abs_self
added
theorem
self_dvd_abs
Renamed
src/algebra/order/ring.lean
to
src/algebra/order/ring/basic.lean
deleted
theorem
abs_cases
deleted
theorem
abs_dvd
deleted
theorem
abs_dvd_abs
deleted
theorem
abs_dvd_self
deleted
theorem
abs_eq_iff_mul_self_eq
deleted
theorem
abs_eq_neg_self
deleted
theorem
abs_eq_self
deleted
def
abs_hom
deleted
theorem
abs_le_iff_mul_self_le
deleted
theorem
abs_le_one_iff_mul_self_le_one
deleted
theorem
abs_lt_iff_mul_self_lt
deleted
theorem
abs_mul
deleted
theorem
abs_mul_abs_self
deleted
theorem
abs_mul_self
deleted
theorem
abs_one
deleted
theorem
abs_sub_sq
deleted
theorem
abs_two
deleted
theorem
canonically_ordered_comm_semiring.mul_pos
deleted
theorem
dvd_abs
deleted
theorem
max_zero_add_max_neg_zero_eq_abs_self
deleted
theorem
mul_add_mul_le_mul_add_mul'
deleted
theorem
mul_add_mul_le_mul_add_mul
deleted
theorem
mul_add_mul_lt_mul_add_mul'
deleted
theorem
mul_add_mul_lt_mul_add_mul
deleted
theorem
mul_tsub
deleted
theorem
self_dvd_abs
deleted
theorem
strict_ordered_semiring.to_char_zero
deleted
theorem
tsub_mul
deleted
theorem
with_bot.bot_lt_mul
deleted
theorem
with_bot.bot_mul
deleted
theorem
with_bot.bot_mul_bot
deleted
theorem
with_bot.coe_mul
deleted
theorem
with_bot.mul_bot
deleted
theorem
with_bot.mul_coe
deleted
theorem
with_bot.mul_def
deleted
theorem
with_bot.mul_eq_bot_iff
deleted
theorem
with_top.coe_mul
deleted
theorem
with_top.mul_coe
deleted
theorem
with_top.mul_def
deleted
theorem
with_top.mul_eq_top_iff
deleted
theorem
with_top.mul_lt_top
deleted
theorem
with_top.mul_top
deleted
theorem
with_top.top_mul
deleted
theorem
with_top.top_mul_top
deleted
theorem
with_top.untop'_zero_mul
Created
src/algebra/order/ring/canonical.lean
added
theorem
canonically_ordered_comm_semiring.mul_pos
added
theorem
mul_add_mul_le_mul_add_mul'
added
theorem
mul_add_mul_le_mul_add_mul
added
theorem
mul_add_mul_lt_mul_add_mul'
added
theorem
mul_add_mul_lt_mul_add_mul
added
theorem
mul_tsub
added
theorem
tsub_mul
Renamed
src/algebra/order/ring_lemmas.lean
to
src/algebra/order/ring/lemmas.lean
Created
src/algebra/order/ring/nontrivial.lean
added
theorem
strict_ordered_semiring.to_char_zero
Created
src/algebra/order/ring/with_top.lean
added
theorem
with_bot.bot_lt_mul
added
theorem
with_bot.bot_mul
added
theorem
with_bot.bot_mul_bot
added
theorem
with_bot.coe_mul
added
theorem
with_bot.mul_bot
added
theorem
with_bot.mul_coe
added
theorem
with_bot.mul_def
added
theorem
with_bot.mul_eq_bot_iff
added
theorem
with_top.coe_mul
added
theorem
with_top.mul_coe
added
theorem
with_top.mul_def
added
theorem
with_top.mul_eq_top_iff
added
theorem
with_top.mul_lt_top
added
theorem
with_top.mul_top
added
theorem
with_top.top_mul
added
theorem
with_top.top_mul_top
added
theorem
with_top.untop'_zero_mul
Modified
src/algebra/order/smul.lean
Modified
src/algebra/order/upper_lower.lean
Modified
src/algebra/order/with_zero.lean
Modified
src/algebra/ring/prod.lean
Modified
src/algebra/tropical/basic.lean
Modified
src/analysis/convex/between.lean
Modified
src/category_theory/differential_object.lean
Modified
src/category_theory/essentially_small.lean
Modified
src/category_theory/limits/shapes/zero_morphisms.lean
Modified
src/category_theory/triangulated/basic.lean
Modified
src/combinatorics/simple_graph/regularity/energy.lean
Modified
src/data/countable/small.lean
Modified
src/data/enat/basic.lean
Modified
src/data/fin/succ_pred.lean
Modified
src/data/fintype/small.lean
Modified
src/data/hash_map.lean
Modified
src/data/int/basic.lean
Modified
src/data/int/order.lean
Modified
src/data/int/succ_pred.lean
Modified
src/data/list/lattice.lean
Modified
src/data/list/min_max.lean
Modified
src/data/list/zip.lean
Modified
src/data/nat/cast.lean
Modified
src/data/nat/order.lean
Modified
src/data/nat/pairing.lean
Modified
src/data/nat/part_enat.lean
Modified
src/data/nat/succ_pred.lean
Modified
src/data/nat/with_bot.lean
Modified
src/data/ordmap/ordset.lean
Modified
src/data/pi/lex.lean
Modified
src/data/pnat/basic.lean
deleted
theorem
nat.nat_pred_succ_pnat
deleted
def
nat.succ_pnat
deleted
theorem
nat.succ_pnat_coe
deleted
def
nat.to_pnat'
deleted
theorem
nat.to_pnat'_coe
deleted
def
nat.to_pnat
deleted
theorem
pnat.coe_eq_one_iff
deleted
theorem
pnat.coe_injective
deleted
theorem
pnat.coe_le_coe
deleted
theorem
pnat.coe_lt_coe
deleted
theorem
pnat.coe_to_pnat'
deleted
def
pnat.div
deleted
theorem
pnat.div_coe
deleted
def
pnat.div_exact
deleted
theorem
pnat.eq
deleted
theorem
pnat.mk_coe
deleted
theorem
pnat.mk_le_mk
deleted
theorem
pnat.mk_lt_mk
deleted
theorem
pnat.mk_one
deleted
def
pnat.mod
deleted
theorem
pnat.mod_coe
deleted
def
pnat.mod_div
deleted
def
pnat.mod_div_aux
deleted
def
pnat.nat_pred
deleted
theorem
pnat.nat_pred_eq_pred
deleted
theorem
pnat.ne_zero
deleted
theorem
pnat.not_lt_one
deleted
theorem
pnat.one_coe
deleted
theorem
pnat.one_le
deleted
theorem
pnat.pos
deleted
def
pnat.strong_induction_on
deleted
theorem
pnat.succ_pnat_nat_pred
deleted
theorem
pnat.to_pnat'_coe
deleted
def
pnat
Created
src/data/pnat/defs.lean
added
theorem
nat.nat_pred_succ_pnat
added
def
nat.succ_pnat
added
theorem
nat.succ_pnat_coe
added
def
nat.to_pnat'
added
theorem
nat.to_pnat'_coe
added
def
nat.to_pnat
added
theorem
pnat.coe_eq_one_iff
added
theorem
pnat.coe_injective
added
theorem
pnat.coe_le_coe
added
theorem
pnat.coe_lt_coe
added
theorem
pnat.coe_to_pnat'
added
def
pnat.div
added
theorem
pnat.div_coe
added
def
pnat.div_exact
added
theorem
pnat.eq
added
theorem
pnat.mk_coe
added
theorem
pnat.mk_le_mk
added
theorem
pnat.mk_lt_mk
added
theorem
pnat.mk_one
added
def
pnat.mod
added
theorem
pnat.mod_coe
added
def
pnat.mod_div
added
def
pnat.mod_div_aux
added
def
pnat.nat_pred
added
theorem
pnat.nat_pred_eq_pred
added
theorem
pnat.ne_zero
added
theorem
pnat.not_lt_one
added
theorem
pnat.one_coe
added
theorem
pnat.one_le
added
theorem
pnat.pos
added
def
pnat.strong_induction_on
added
theorem
pnat.succ_pnat_nat_pred
added
theorem
pnat.to_pnat'_coe
added
def
pnat
Modified
src/data/pnat/interval.lean
Modified
src/data/rat/defs.lean
Modified
src/data/rat/order.lean
Modified
src/data/real/cardinality.lean
Modified
src/data/set/basic.lean
added
theorem
set.nat.mem_range_succ
Modified
src/data/set/intervals/basic.lean
deleted
def
order_iso.Ici_bot
deleted
def
order_iso.Iic_top
deleted
theorem
order_iso.image_Icc
deleted
theorem
order_iso.image_Ici
deleted
theorem
order_iso.image_Ico
deleted
theorem
order_iso.image_Iic
deleted
theorem
order_iso.image_Iio
deleted
theorem
order_iso.image_Ioc
deleted
theorem
order_iso.image_Ioi
deleted
theorem
order_iso.image_Ioo
deleted
theorem
order_iso.preimage_Icc
deleted
theorem
order_iso.preimage_Ici
deleted
theorem
order_iso.preimage_Ico
deleted
theorem
order_iso.preimage_Iic
deleted
theorem
order_iso.preimage_Iio
deleted
theorem
order_iso.preimage_Ioc
deleted
theorem
order_iso.preimage_Ioi
deleted
theorem
order_iso.preimage_Ioo
deleted
theorem
set.add_mem_Icc_iff_left
deleted
theorem
set.add_mem_Icc_iff_right
deleted
theorem
set.add_mem_Ico_iff_left
deleted
theorem
set.add_mem_Ico_iff_right
deleted
theorem
set.add_mem_Ioc_iff_left
deleted
theorem
set.add_mem_Ioc_iff_right
deleted
theorem
set.add_mem_Ioo_iff_left
deleted
theorem
set.add_mem_Ioo_iff_right
deleted
theorem
set.inv_mem_Icc_iff
deleted
theorem
set.inv_mem_Ico_iff
deleted
theorem
set.inv_mem_Ioc_iff
deleted
theorem
set.inv_mem_Ioo_iff
deleted
theorem
set.mem_Icc_iff_abs_le
deleted
theorem
set.nonempty_Ico_sdiff
deleted
theorem
set.sub_mem_Icc_iff_left
deleted
theorem
set.sub_mem_Icc_iff_right
deleted
theorem
set.sub_mem_Ico_iff_left
deleted
theorem
set.sub_mem_Ico_iff_right
deleted
theorem
set.sub_mem_Ioc_iff_left
deleted
theorem
set.sub_mem_Ioc_iff_right
deleted
theorem
set.sub_mem_Ioo_iff_left
deleted
theorem
set.sub_mem_Ioo_iff_right
Created
src/data/set/intervals/group.lean
added
theorem
set.add_mem_Icc_iff_left
added
theorem
set.add_mem_Icc_iff_right
added
theorem
set.add_mem_Ico_iff_left
added
theorem
set.add_mem_Ico_iff_right
added
theorem
set.add_mem_Ioc_iff_left
added
theorem
set.add_mem_Ioc_iff_right
added
theorem
set.add_mem_Ioo_iff_left
added
theorem
set.add_mem_Ioo_iff_right
added
theorem
set.inv_mem_Icc_iff
added
theorem
set.inv_mem_Ico_iff
added
theorem
set.inv_mem_Ioc_iff
added
theorem
set.inv_mem_Ioo_iff
added
theorem
set.mem_Icc_iff_abs_le
added
theorem
set.nonempty_Ico_sdiff
added
theorem
set.sub_mem_Icc_iff_left
added
theorem
set.sub_mem_Icc_iff_right
added
theorem
set.sub_mem_Ico_iff_left
added
theorem
set.sub_mem_Ico_iff_right
added
theorem
set.sub_mem_Ioc_iff_left
added
theorem
set.sub_mem_Ioc_iff_right
added
theorem
set.sub_mem_Ioo_iff_left
added
theorem
set.sub_mem_Ioo_iff_right
Modified
src/data/set/intervals/ord_connected_component.lean
Created
src/data/set/intervals/order_iso.lean
added
def
order_iso.Ici_bot
added
def
order_iso.Iic_top
added
theorem
order_iso.image_Icc
added
theorem
order_iso.image_Ici
added
theorem
order_iso.image_Ico
added
theorem
order_iso.image_Iic
added
theorem
order_iso.image_Iio
added
theorem
order_iso.image_Ioc
added
theorem
order_iso.image_Ioi
added
theorem
order_iso.image_Ioo
added
theorem
order_iso.preimage_Icc
added
theorem
order_iso.preimage_Ici
added
theorem
order_iso.preimage_Ico
added
theorem
order_iso.preimage_Iic
added
theorem
order_iso.preimage_Iio
added
theorem
order_iso.preimage_Ioc
added
theorem
order_iso.preimage_Ioi
added
theorem
order_iso.preimage_Ioo
Modified
src/data/set/intervals/unordered_interval.lean
deleted
theorem
set.abs_sub_le_of_subinterval
deleted
theorem
set.abs_sub_left_of_mem_interval
deleted
theorem
set.abs_sub_right_of_mem_interval
deleted
theorem
set.image_add_const_interval
deleted
theorem
set.image_const_add_interval
deleted
theorem
set.image_const_mul_interval
deleted
theorem
set.image_const_sub_interval
deleted
theorem
set.image_div_const_interval
deleted
theorem
set.image_mul_const_interval
deleted
theorem
set.image_neg_interval
deleted
theorem
set.image_sub_const_interval
deleted
theorem
set.preimage_add_const_interval
deleted
theorem
set.preimage_const_add_interval
deleted
theorem
set.preimage_const_mul_interval
deleted
theorem
set.preimage_const_sub_interval
deleted
theorem
set.preimage_div_const_interval
deleted
theorem
set.preimage_mul_const_interval
deleted
theorem
set.preimage_neg_interval
deleted
theorem
set.preimage_sub_const_interval
Modified
src/data/set/pairwise.lean
deleted
theorem
function.injective_iff_pairwise_ne
deleted
theorem
pairwise.mono
deleted
theorem
pairwise.set_pairwise
deleted
def
pairwise
deleted
theorem
reflexive.set_pairwise_iff
deleted
theorem
set.pairwise.imp
deleted
theorem
set.pairwise.imp_on
deleted
theorem
set.pairwise.on_injective
deleted
theorem
set.pairwise_of_forall
Renamed
src/data/set/intervals/image_preimage.lean
to
src/data/set/pointwise/interval.lean
added
theorem
set.abs_sub_le_of_subinterval
added
theorem
set.abs_sub_left_of_mem_interval
added
theorem
set.abs_sub_right_of_mem_interval
added
theorem
set.image_add_const_interval
modified
theorem
set.image_affine_Icc'
added
theorem
set.image_const_add_interval
added
theorem
set.image_const_mul_interval
added
theorem
set.image_const_sub_interval
added
theorem
set.image_div_const_interval
added
theorem
set.image_mul_const_interval
modified
theorem
set.image_mul_left_Icc'
modified
theorem
set.image_mul_left_Icc
modified
theorem
set.image_mul_left_Ioo
modified
theorem
set.image_mul_right_Icc'
modified
theorem
set.image_mul_right_Icc
modified
theorem
set.image_mul_right_Ioo
added
theorem
set.image_neg_interval
added
theorem
set.image_sub_const_interval
modified
theorem
set.inv_Ioi
modified
theorem
set.inv_Ioo_0_left
added
theorem
set.preimage_add_const_interval
added
theorem
set.preimage_const_add_interval
modified
theorem
set.preimage_const_mul_Icc
modified
theorem
set.preimage_const_mul_Icc_of_neg
modified
theorem
set.preimage_const_mul_Ici
modified
theorem
set.preimage_const_mul_Ici_of_neg
modified
theorem
set.preimage_const_mul_Ico
modified
theorem
set.preimage_const_mul_Ico_of_neg
modified
theorem
set.preimage_const_mul_Iic
modified
theorem
set.preimage_const_mul_Iic_of_neg
modified
theorem
set.preimage_const_mul_Iio
modified
theorem
set.preimage_const_mul_Iio_of_neg
modified
theorem
set.preimage_const_mul_Ioc
modified
theorem
set.preimage_const_mul_Ioc_of_neg
modified
theorem
set.preimage_const_mul_Ioi
modified
theorem
set.preimage_const_mul_Ioi_of_neg
modified
theorem
set.preimage_const_mul_Ioo
modified
theorem
set.preimage_const_mul_Ioo_of_neg
added
theorem
set.preimage_const_mul_interval
added
theorem
set.preimage_const_sub_interval
added
theorem
set.preimage_div_const_interval
modified
theorem
set.preimage_mul_const_Icc
modified
theorem
set.preimage_mul_const_Icc_of_neg
modified
theorem
set.preimage_mul_const_Ici
modified
theorem
set.preimage_mul_const_Ici_of_neg
modified
theorem
set.preimage_mul_const_Ico
modified
theorem
set.preimage_mul_const_Ico_of_neg
modified
theorem
set.preimage_mul_const_Iic
modified
theorem
set.preimage_mul_const_Iic_of_neg
modified
theorem
set.preimage_mul_const_Iio
modified
theorem
set.preimage_mul_const_Iio_of_neg
modified
theorem
set.preimage_mul_const_Ioc
modified
theorem
set.preimage_mul_const_Ioc_of_neg
modified
theorem
set.preimage_mul_const_Ioi
modified
theorem
set.preimage_mul_const_Ioi_of_neg
modified
theorem
set.preimage_mul_const_Ioo
modified
theorem
set.preimage_mul_const_Ioo_of_neg
added
theorem
set.preimage_mul_const_interval
added
theorem
set.preimage_neg_interval
added
theorem
set.preimage_sub_const_interval
Modified
src/dynamics/periodic_pts.lean
Modified
src/group_theory/submonoid/operations.lean
Modified
src/group_theory/subsemigroup/operations.lean
Modified
src/linear_algebra/affine_space/affine_map.lean
Modified
src/linear_algebra/free_module/basic.lean
Modified
src/logic/encodable/basic.lean
Modified
src/logic/equiv/nat.lean
Created
src/logic/pairwise.lean
added
theorem
function.injective_iff_pairwise_ne
added
theorem
pairwise.mono
added
theorem
pairwise.set_pairwise
added
def
pairwise
added
theorem
reflexive.set_pairwise_iff
added
theorem
set.pairwise.imp
added
theorem
set.pairwise.imp_on
added
theorem
set.pairwise.on_injective
added
theorem
set.pairwise_of_forall
Renamed
src/logic/small.lean
to
src/logic/small/basic.lean
Created
src/logic/small/list.lean
Modified
src/model_theory/basic.lean
Modified
src/number_theory/ADE_inequality.lean
Modified
src/number_theory/lucas_lehmer.lean
Modified
src/order/atoms.lean
Modified
src/order/basic.lean
Renamed
src/order/bounds.lean
to
src/order/bounds/basic.lean
deleted
theorem
is_glb.exists_between_self_add'
deleted
theorem
is_glb.exists_between_self_add
deleted
theorem
is_lub.exists_between_sub_self'
deleted
theorem
is_lub.exists_between_sub_self
deleted
theorem
order_iso.is_glb_image'
deleted
theorem
order_iso.is_glb_image
deleted
theorem
order_iso.is_glb_preimage'
deleted
theorem
order_iso.is_glb_preimage
deleted
theorem
order_iso.is_lub_image'
deleted
theorem
order_iso.is_lub_image
deleted
theorem
order_iso.is_lub_preimage'
deleted
theorem
order_iso.is_lub_preimage
deleted
theorem
order_iso.lower_bounds_image
deleted
theorem
order_iso.upper_bounds_image
Created
src/order/bounds/order_iso.lean
added
theorem
order_iso.is_glb_image'
added
theorem
order_iso.is_glb_image
added
theorem
order_iso.is_glb_preimage'
added
theorem
order_iso.is_glb_preimage
added
theorem
order_iso.is_lub_image'
added
theorem
order_iso.is_lub_image
added
theorem
order_iso.is_lub_preimage'
added
theorem
order_iso.is_lub_preimage
added
theorem
order_iso.lower_bounds_image
added
theorem
order_iso.upper_bounds_image
Modified
src/order/compactly_generated.lean
Modified
src/order/complete_lattice.lean
Modified
src/order/conditionally_complete_lattice.lean
Modified
src/order/filter/at_top_bot.lean
Modified
src/order/lattice_intervals.lean
Modified
src/order/semiconj_Sup.lean
Modified
src/order/succ_pred/interval_succ.lean
Modified
src/order/upper_lower.lean
Modified
src/ring_theory/hahn_series.lean
Modified
src/set_theory/cardinal/basic.lean
Modified
src/set_theory/zfc/basic.lean
Modified
src/tactic/interval_cases.lean
Modified
src/tactic/linarith/lemmas.lean
Modified
src/tactic/monotonicity/lemmas.lean
Modified
src/testing/slim_check/sampleable.lean
Modified
src/topology/algebra/order/basic.lean
Modified
src/topology/instances/real.lean
Modified
test/finish4.lean
Modified
test/library_search/ordered_ring.lean
Modified
test/monotonicity.lean
Modified
test/nontriviality.lean
Modified
test/squeeze.lean