Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-09 04:01 796efae2

View on Github →

feat(data/real/sqrt): nnreal.coe_sqrt and nnreal.sqrt_eq_rpow (#9025) Also rename a few lemmas:

  • nnreal.mul_sqrt_self -> nnreal.mul_self_sqrt to follow real.mul_self_sqrt
  • real.sqrt_le -> real.sqrt_le_sqrt_iff
  • real.sqrt_lt -> real.sqrt_lt_sqrt_iff and provide a few more for commodity:
  • nnreal.sqrt_sq
  • nnreal.sq_sqrt
  • real.sqrt_lt_sqrt
  • real.sqrt_lt_sqrt_iff_of_pos
  • nnreal.sqrt_le_sqrt_iff
  • nnreal.sqrt_lt_sqrt_iff Closes #8016

Estimated changes

added theorem nnreal.sqrt_eq_rpow
modified theorem real.sqrt_eq_rpow
added theorem nnreal.mul_self_sqrt
deleted theorem nnreal.mul_sqrt_self
added theorem nnreal.sq_sqrt
added theorem nnreal.sqrt_sq
added theorem real.coe_sqrt
modified theorem real.sq_sqrt
deleted theorem real.sqrt_le
added theorem real.sqrt_le_sqrt_iff
deleted theorem real.sqrt_lt
added theorem real.sqrt_lt_sqrt
added theorem real.sqrt_lt_sqrt_iff