<commit_before>/-
Copyright (c) 2022 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/

import algebra.ring.basic
import algebra.algebra.basic
import algebra.group_power.basic
import algebra.field_power
import algebra.opposites

/-!  # Squares, even and odd elements

This file proves some general facts about squares, even and odd elements of semirings.

In the implementation, we define `is_square` and we let `even` be the notion transported by
`to_additive`.  The definition are therefore as follows:
```lean
is_square a ↔ ∃ r, a = r * r
even a ↔ ∃ r, a = r + r
```

Odd elements are not unified with a multiplicative notion.

## Future work

* TODO: Try to generalize further the typeclass assumptions on `is_square/even`.
  For instance, in some cases, there are `semiring` assumptions that I (DT) am not convinced are
  necessary.
* TODO: Consider moving the definition and lemmas about `odd` to a separate file.
* TODO: The "old" definition of `even a` asked for the existence of an element `c` such that
  `a = 2 * c`.  For this reason, several fixes introduce an extra `two_mul` or `← two_mul`.
  It might be the case that by making a careful choice of `simp` lemma, this can be avoided.
 -/

open mul_opposite
variables {F α β R : Type*}

section has_mul
variables [has_mul α]

/--  An element `a` of a type `α` with multiplication satisfies `square a` if `a = r * r`,
for some `r : α`. -/
@[to_additive
"An element `a` of a type `α` with addition satisfies `even a` if `a = r + r`,
for some `r : α`."]
def is_square (a : α) : Prop := ∃ r, a = r * r

@[simp, to_additive] lemma is_square_mul_self (m : α) : is_square (m * m) := ⟨m, rfl⟩

@[to_additive] lemma is_square_op_iff (a : α) : is_square (op a) ↔ is_square a :=
⟨λ ⟨c, hc⟩, ⟨unop c, by rw [← unop_mul, ← hc, unop_op]⟩, λ ⟨c, hc⟩, by simp [hc]⟩

/-- Create a decidability instance for `is_square` on `fintype`s. -/
instance is_square_decidable [fintype α] [decidable_eq α] : decidable_pred (is_square : α → Prop) :=
λ a, fintype.decidable_exists_fintype

end has_mul

@[simp, to_additive]
lemma is_square_one [mul_one_class α] : is_square (1 : α) := ⟨1, (mul_one _).symm⟩

@[to_additive]
lemma is_square.map [mul_one_class α] [mul_one_class β] [monoid_hom_class F α β] {m : α} (f : F) :
  is_square m → is_square (f m) :=
by { rintro ⟨m, rfl⟩, exact ⟨f m, by simp⟩ }

section monoid
variables [monoid α]

@[to_additive even_iff_exists_two_nsmul]
lemma is_square_iff_exists_sq (m : α) : is_square m ↔ ∃ c, m = c ^ 2 :=
by simp [is_square, pow_two]

alias is_square_iff_exists_sq ↔ is_square.exists_sq is_square_of_exists_sq

attribute [to_additive even.exists_two_nsmul "Alias of the forwards direction of
`even_iff_exists_two_nsmul`."] is_square.exists_sq

attribute [to_additive even_of_exists_two_nsmul "Alias of the backwards direction of
`even_iff_exists_two_nsmul`."] is_square_of_exists_sq

@[simp, to_additive even_two_nsmul]
lemma is_square_sq (a : α) : is_square (a ^ 2) := ⟨a, pow_two _⟩

variables [has_distrib_neg α] {n : ℕ}

lemma even.neg_pow : even n → ∀ a : α, (-a) ^ n = a ^ n :=
by { rintro ⟨c, rfl⟩ a, simp_rw [←two_mul, pow_mul, neg_sq] }

lemma even.neg_one_pow (h : even n) : (-1 : α) ^ n = 1 := by rw [h.neg_pow, one_pow]

end monoid

/-- `0` is always a square (in a monoid with zero). -/
lemma is_square_zero (M : Type*) [monoid_with_zero M] : is_square (0 : M) :=
by { use 0, simp only [mul_zero] }

@[to_additive] lemma is_square.mul [comm_semigroup α] {a b : α} :
  is_square a → is_square b → is_square (a * b) :=
by { rintro ⟨a, rfl⟩ ⟨b, rfl⟩, exact ⟨a * b, mul_mul_mul_comm _ _ _ _⟩ }

section division_monoid
variables [division_monoid α] {a : α}

@[simp, to_additive] lemma is_square_inv : is_square a⁻¹ ↔ is_square a :=
begin
  refine ⟨λ h, _, λ h, _⟩,
  { rw [← is_square_op_iff, ← inv_inv a],
    exact h.map (mul_equiv.inv' α) },
  { exact ((is_square_op_iff a).mpr h).map (mul_equiv.inv' α).symm }
end

alias is_square_inv ↔ _ is_square.inv

attribute [to_additive] is_square.inv

variables [has_distrib_neg α] {n : ℤ}

lemma even.neg_zpow : even n → ∀ a : α, (-a) ^ n = a ^ n :=
by { rintro ⟨c, rfl⟩ a, exact zpow_bit0_neg _ _ }

lemma even.neg_one_zpow (h : even n) : (-1 : α) ^ n = 1 := by rw [h.neg_zpow, one_zpow]

end division_monoid

lemma even_abs [subtraction_monoid α] [linear_order α] {a : α} : even (|a|) ↔ even a :=
by cases abs_choice a; simp only [h, even_neg]

@[to_additive]
lemma is_square.div [division_comm_monoid α] {a b : α} (ha : is_square a) (hb : is_square b) :
  is_square (a / b) :=
by { rw div_eq_mul_inv, exact ha.mul hb.inv }

-- `odd.tsub` requires `canonically_linear_ordered_semiring`, which we don't have
lemma even.tsub [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α]
  [contravariant_class α α (+) (≤)] {m n : α} (hm : even m) (hn : even n) : even (m - n) :=
begin
  obtain ⟨a, rfl⟩ := hm,
  obtain ⟨b, rfl⟩ := hn,
  refine ⟨a - b, _⟩,
  obtain h | h := le_total a b,
  { rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero] },
  { exact (tsub_add_tsub_comm h h).symm }
end

lemma even_iff_exists_bit0 [has_add α] {a : α} : even a ↔ ∃ b, a = bit0 b := iff.rfl

alias even_iff_exists_bit0 ↔ even.exists_bit0 _

section semiring
variables [semiring α] [semiring β] {m n : α}
<commit_msg>feat(algebra/parity): Primes are not square (#16430)<commit_after>/-
Copyright (c) 2022 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/

import algebra.ring.basic
import algebra.algebra.basic
import algebra.group_power.basic
import algebra.field_power
import algebra.opposites

/-!  # Squares, even and odd elements

This file proves some general facts about squares, even and odd elements of semirings.

In the implementation, we define `is_square` and we let `even` be the notion transported by
`to_additive`.  The definition are therefore as follows:
```lean
is_square a ↔ ∃ r, a = r * r
even a ↔ ∃ r, a = r + r
```

Odd elements are not unified with a multiplicative notion.

## Future work

* TODO: Try to generalize further the typeclass assumptions on `is_square/even`.
  For instance, in some cases, there are `semiring` assumptions that I (DT) am not convinced are
  necessary.
* TODO: Consider moving the definition and lemmas about `odd` to a separate file.
* TODO: The "old" definition of `even a` asked for the existence of an element `c` such that
  `a = 2 * c`.  For this reason, several fixes introduce an extra `two_mul` or `← two_mul`.
  It might be the case that by making a careful choice of `simp` lemma, this can be avoided.
 -/

open mul_opposite
variables {F α β R : Type*}

section has_mul
variables [has_mul α]

/--  An element `a` of a type `α` with multiplication satisfies `square a` if `a = r * r`,
for some `r : α`. -/
@[to_additive
"An element `a` of a type `α` with addition satisfies `even a` if `a = r + r`,
for some `r : α`."]
def is_square (a : α) : Prop := ∃ r, a = r * r

@[simp, to_additive] lemma is_square_mul_self (m : α) : is_square (m * m) := ⟨m, rfl⟩

@[to_additive] lemma is_square_op_iff (a : α) : is_square (op a) ↔ is_square a :=
⟨λ ⟨c, hc⟩, ⟨unop c, by rw [← unop_mul, ← hc, unop_op]⟩, λ ⟨c, hc⟩, by simp [hc]⟩

/-- Create a decidability instance for `is_square` on `fintype`s. -/
instance is_square_decidable [fintype α] [decidable_eq α] : decidable_pred (is_square : α → Prop) :=
λ a, fintype.decidable_exists_fintype

end has_mul

@[simp, to_additive]
lemma is_square_one [mul_one_class α] : is_square (1 : α) := ⟨1, (mul_one _).symm⟩

@[to_additive]
lemma is_square.map [mul_one_class α] [mul_one_class β] [monoid_hom_class F α β] {m : α} (f : F) :
  is_square m → is_square (f m) :=
by { rintro ⟨m, rfl⟩, exact ⟨f m, by simp⟩ }

section monoid
variables [monoid α] {n : ℕ} {a : α}

@[to_additive even_iff_exists_two_nsmul]
lemma is_square_iff_exists_sq (m : α) : is_square m ↔ ∃ c, m = c ^ 2 :=
by simp [is_square, pow_two]

alias is_square_iff_exists_sq ↔ is_square.exists_sq is_square_of_exists_sq

attribute [to_additive even.exists_two_nsmul "Alias of the forwards direction of
`even_iff_exists_two_nsmul`."] is_square.exists_sq

attribute [to_additive even_of_exists_two_nsmul "Alias of the backwards direction of
`even_iff_exists_two_nsmul`."] is_square_of_exists_sq

@[to_additive even.nsmul] lemma is_square.pow (n : ℕ) : is_square a → is_square (a ^ n) :=
by { rintro ⟨a, rfl⟩, exact ⟨a ^ n, (commute.refl _).mul_pow _⟩ }

@[simp, to_additive even.nsmul']
lemma even.is_square_pow : even n → ∀ a : α, is_square (a ^ n) :=
by { rintro ⟨n, rfl⟩ a, exact ⟨a ^ n, pow_add _ _ _⟩ }

@[simp, to_additive even_two_nsmul]
lemma is_square_sq (a : α) : is_square (a ^ 2) := ⟨a, pow_two _⟩

variables [has_distrib_neg α]

lemma even.neg_pow : even n → ∀ a : α, (-a) ^ n = a ^ n :=
by { rintro ⟨c, rfl⟩ a, simp_rw [←two_mul, pow_mul, neg_sq] }

lemma even.neg_one_pow (h : even n) : (-1 : α) ^ n = 1 := by rw [h.neg_pow, one_pow]

end monoid

@[to_additive] lemma is_square.mul [comm_semigroup α] {a b : α} :
  is_square a → is_square b → is_square (a * b) :=
by { rintro ⟨a, rfl⟩ ⟨b, rfl⟩, exact ⟨a * b, mul_mul_mul_comm _ _ _ _⟩ }

section comm_monoid
variables [comm_monoid α] {a : α}

lemma irreducible.not_square (ha : irreducible a) : ¬ is_square a :=
by { rintro ⟨b, rfl⟩, simp only [irreducible_mul_iff, or_self] at ha, exact ha.1.not_unit ha.2 }

lemma is_square.not_irreducible (ha : is_square a) : ¬ irreducible a := λ h, h.not_square ha

end comm_monoid

variables (α)

@[simp] lemma is_square_zero [mul_zero_class α] : is_square (0 : α) := ⟨0, (mul_zero _).symm⟩

variables {α}

section cancel_comm_monoid_with_zero
variables [cancel_comm_monoid_with_zero α] {a : α}

lemma prime.not_square (ha : prime a) : ¬ is_square a := ha.irreducible.not_square
lemma is_square.not_prime (ha : is_square a) : ¬ prime a := λ h, h.not_square ha

end cancel_comm_monoid_with_zero

section division_monoid
variables [division_monoid α] {a : α}

@[simp, to_additive] lemma is_square_inv : is_square a⁻¹ ↔ is_square a :=
begin
  refine ⟨λ h, _, λ h, _⟩,
  { rw [← is_square_op_iff, ← inv_inv a],
    exact h.map (mul_equiv.inv' α) },
  { exact ((is_square_op_iff a).mpr h).map (mul_equiv.inv' α).symm }
end

alias is_square_inv ↔ _ is_square.inv

attribute [to_additive] is_square.inv

@[to_additive even.zsmul] lemma is_square.zpow (n : ℤ) : is_square a → is_square (a ^ n) :=
by { rintro ⟨a, rfl⟩, exact ⟨a ^ n, (commute.refl _).mul_zpow _⟩ }

variables [has_distrib_neg α] {n : ℤ}

lemma even.neg_zpow : even n → ∀ a : α, (-a) ^ n = a ^ n :=
by { rintro ⟨c, rfl⟩ a, exact zpow_bit0_neg _ _ }

lemma even.neg_one_zpow (h : even n) : (-1 : α) ^ n = 1 := by rw [h.neg_zpow, one_zpow]

end division_monoid

lemma even_abs [subtraction_monoid α] [linear_order α] {a : α} : even (|a|) ↔ even a :=
by cases abs_choice a; simp only [h, even_neg]

@[to_additive]
lemma is_square.div [division_comm_monoid α] {a b : α} (ha : is_square a) (hb : is_square b) :
  is_square (a / b) :=
by { rw div_eq_mul_inv, exact ha.mul hb.inv }

@[simp, to_additive even.zsmul']
lemma even.is_square_zpow [group α] {n : ℤ} : even n → ∀ a : α, is_square (a ^ n) :=
by { rintro ⟨n, rfl⟩ a, exact ⟨a ^ n, zpow_add _ _ _⟩ }

-- `odd.tsub` requires `canonically_linear_ordered_semiring`, which we don't have
lemma even.tsub [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α]
  [contravariant_class α α (+) (≤)] {m n : α} (hm : even m) (hn : even n) : even (m - n) :=
begin
  obtain ⟨a, rfl⟩ := hm,
  obtain ⟨b, rfl⟩ := hn,
  refine ⟨a - b, _⟩,
  obtain h | h := le_total a b,
  { rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero] },
  { exact (tsub_add_tsub_comm h h).symm }
end

lemma even_iff_exists_bit0 [has_add α] {a : α} : even a ↔ ∃ b, a = bit0 b := iff.rfl

alias even_iff_exists_bit0 ↔ even.exists_bit0 _

section semiring
variables [semiring α] [semiring β] {m n : α}

{'fraction_non_alphanumeric': 0.12819010961425822, 'fraction_numerical': 0.0043511003263325245, 'mean_word_length': 4.036662452591656, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1744562', 'n_tokens_mistral': 5115, 'n_tokens_neox': 4982, 'n_words': 1643}