Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-21 14:11 86b9ee4e

View on Github →

feat(algebra|data): misc lemmas in low-level files (#16948)

From the sphere eversion project

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem finset.equiv.prod_comp_finset

Modified src/algebra/big_operators/finprod.lean

added theorem finprod_comp_equiv

Modified src/algebra/group/prod.lean

added theorem prod.mk_one_mul_mk_one

added theorem prod.one_mk_mul_one_mk

Modified src/algebra/module/basic.lean

added theorem smul_add_one_sub_smul

Modified src/algebra/order/group/basic.lean

added theorem abs_le_abs_of_nonneg

added theorem abs_le_abs_of_nonpos

Modified src/data/real/nnreal.lean

added theorem real.nnabs_coe

Modified src/data/set/finite.lean

added theorem set.finite_of_finite_preimage

Modified src/data/set/function.lean

added theorem function.injective.inj_on_range

Modified src/group_theory/group_action/prod.lean

added theorem prod.smul_mk_zero

added theorem prod.smul_zero_mk