Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-29 14:39 a3beb628

View on Github →

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

Estimated changes

Modified src/analysis/inner_product_space/pi_L2.lean

Modified src/analysis/special_functions/pow.lean

modified theorem complex.cpow_int_cast

modified theorem complex.cpow_nat_cast

added theorem complex.cpow_two

added theorem ennreal.rpow_two

added theorem nnreal.rpow_two

added theorem real.rpow_two

Modified src/analysis/specific_limits/basic.lean

added theorem tendsto_nat_ceil_div_at_top

added theorem tendsto_nat_floor_at_top

added theorem tendsto_nat_floor_div_at_top

Modified src/data/real/ennreal.lean

added theorem ennreal.one_le_two

Modified src/topology/algebra/group.lean

added theorem tendsto_div_nhds_one_iff