Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-30 11:26 26310e71

View on Github →

feat(algebra/*): a sample of easy useful lemmas (#13696) Lemmas needed for #13690

Estimated changes

Modified src/algebra/big_operators/intervals.lean

added theorem finset.prod_Ioc_consecutive

added theorem finset.prod_Ioc_succ_top

Modified src/algebra/geom_sum.lean

added theorem geom_sum_Ico_le_of_lt_one

Modified src/algebra/group_power/basic.lean

added theorem add_sq'

added theorem sub_sq'

Modified src/algebra/order/floor.lean

added theorem nat.one_le_floor_iff

Modified src/algebra/order/group.lean

added theorem neg_abs_le_neg

Modified src/data/finset/locally_finite.lean

added theorem finset.Ioc_union_Ioc_eq_Ioc

Modified src/data/nat/interval.lean

added theorem nat.Ioc_succ_singleton