Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-28 19:37 b9c80c92

View on Github →

chore(*): use sq as convention for "squared" (#7368) This PR establishes sq x as the notation for x ^ 2. See this Zulip conversation. A breakdown of the refactor:

  • All instances of square and sqr are changed to sq (except where square means something other than "to the second power")
  • All instances of pow_two are changed to sq, though many are kept are aliases
  • All instances of sum_of_two_squares are changed to sq_add_sq n.b. I did NOT alter any instances of:
  • squarefree
  • sum_of_four_squares
  • fpow_two or rpow_two
<!-- The text above the `

Estimated changes

deleted theorem nat.eq_pow_two_mul_odd
added theorem nat.eq_two_pow_mul_odd
added theorem abs_le_abs_of_sq_le_sq
deleted theorem abs_le_abs_of_sqr_le_sqr
added theorem abs_le_of_sq_le_sq'
added theorem abs_le_of_sq_le_sq
deleted theorem abs_le_of_sqr_le_sqr'
deleted theorem abs_le_of_sqr_le_sqr
added theorem abs_lt_abs_of_sq_lt_sq
deleted theorem abs_lt_abs_of_sqr_lt_sqr
added theorem abs_lt_of_sq_lt_sq'
added theorem abs_lt_of_sq_lt_sq
deleted theorem abs_lt_of_sqr_lt_sqr'
deleted theorem abs_lt_of_sqr_lt_sqr
added theorem abs_sq
deleted theorem abs_sqr
deleted theorem add_pow_two
added theorem add_sq
deleted theorem eq_of_pow_two_eq_pow_two
added theorem eq_of_sq_eq_sq
added theorem neg_sq
deleted theorem neg_square
deleted theorem pow_two_nonneg
deleted theorem pow_two_pos_of_ne_zero
deleted theorem pow_two_sub_pow_two
added theorem sq_abs
added theorem sq_le_sq'
added theorem sq_le_sq
added theorem sq_lt_sq'
added theorem sq_lt_sq
added theorem sq_nonneg
added theorem sq_pos_of_ne_zero
modified theorem sq_sub_sq
deleted theorem sqr_abs
deleted theorem sqr_le_sqr'
deleted theorem sqr_le_sqr
deleted theorem sqr_lt_sqr'
deleted theorem sqr_lt_sqr
deleted theorem sub_pow_two
added theorem sub_sq
deleted theorem two_mul_le_add_pow_two
added theorem two_mul_le_add_sq
deleted theorem int.abs_le_self_pow_two
added theorem int.abs_le_self_sq
deleted theorem int.le_self_pow_two
added theorem int.le_self_sq
deleted theorem int.nat_abs_pow_two
added theorem int.nat_abs_sq
deleted theorem int.units_pow_two
added theorem int.units_sq
modified theorem one_add_mul_le_pow'
added theorem abs_sub_sq
deleted theorem abs_sub_square
added theorem differentiable.norm_sq
added theorem inner_self_eq_norm_sq
deleted theorem inner_self_eq_norm_square
deleted theorem norm_add_pow_two
deleted theorem norm_add_pow_two_real
added theorem norm_add_sq
added theorem norm_add_sq_real
deleted theorem norm_sub_pow_two
deleted theorem norm_sub_pow_two_real
added theorem norm_sub_sq
added theorem norm_sub_sq_real
added theorem real.sq_cos_pi_div_six
added theorem colex.sum_sq_lt_iff_lt
deleted theorem nat.sum_pow_two_lt
added theorem nat.sum_sq_lt
modified theorem complex.I_sq
added theorem complex.cos_sq'
added theorem complex.cos_sq
deleted theorem complex.cos_square'
deleted theorem complex.cos_square
added theorem complex.cosh_sq
deleted theorem complex.cosh_square
added theorem complex.sin_sq
deleted theorem complex.sin_square
added theorem complex.sinh_sq
deleted theorem complex.sinh_square
added theorem real.cos_sq'
added theorem real.cos_sq
deleted theorem real.cos_square'
deleted theorem real.cos_square
added theorem real.cosh_sq
deleted theorem real.cosh_square
added theorem real.sin_sq
deleted theorem real.sin_square
added theorem real.sinh_sq
deleted theorem real.sinh_square
modified theorem is_R_or_C.norm_sq_to_real
deleted theorem nat.pow_two_sub_pow_two
added theorem nat.sq_sub_sq
deleted theorem nat.neg_one_pow_two
added theorem nat.neg_one_sq
deleted theorem nnreal.sqrt_eq_iff_sqr_eq
modified theorem nnreal.sqrt_one
added theorem real.le_sqrt_of_sq_le
deleted theorem real.le_sqrt_of_sqr_le
added theorem real.lt_sqrt_of_sq_lt
deleted theorem real.lt_sqrt_of_sqr_lt
added theorem real.sq_le
added theorem real.sq_lt
added theorem real.sq_sqrt
deleted theorem real.sqr_le
deleted theorem real.sqr_lt
deleted theorem real.sqr_sqrt
added theorem real.sqrt_eq_iff_sq_eq
deleted theorem real.sqrt_eq_iff_sqr_eq
added theorem real.sqrt_sq
added theorem real.sqrt_sq_eq_abs
deleted theorem real.sqrt_sqr
deleted theorem real.sqrt_sqr_eq_abs
added theorem zsqrtd.not_divides_sq
deleted theorem zsqrtd.not_divides_square
added theorem char_p.sq_add_sq
deleted theorem char_p.sum_two_squares
added theorem zmod.sq_add_sq
deleted theorem zmod.sum_two_squares
added theorem quaternion_group.xa_sq
added theorem int.coprime_of_sq_sum'
added theorem int.coprime_of_sq_sum
deleted theorem int.coprime_of_sqr_sum'
deleted theorem int.coprime_of_sqr_sum
added theorem nat.prime.sq_add_sq
deleted theorem nat.prime.sum_two_squares
added theorem int.sq_of_coprime
added theorem int.sq_of_gcd_eq_one
deleted theorem int.sqr_of_coprime
deleted theorem int.sqr_of_gcd_eq_one