diff --git a/src/algebra/parity.lean b/src/algebra/parity.lean index 6c65fb9f65854..07a69fc759459 100644 --- a/src/algebra/parity.lean +++ b/src/algebra/parity.lean @@ -67,7 +67,7 @@ lemma is_square.map [mul_one_class α] [mul_one_class β] [monoid_hom_class F α by { rintro ⟨m, rfl⟩, exact ⟨f m, by simp⟩ } section monoid -variables [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 := @@ -81,10 +81,17 @@ attribute [to_additive even.exists_two_nsmul "Alias of the forwards direction of 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 α] {n : ℕ} +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] } @@ -93,14 +100,34 @@ lemma even.neg_one_pow (h : even n) : (-1 : α) ^ n = 1 := by rw [h.neg_pow, one 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 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 : α} @@ -116,6 +143,9 @@ 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 := @@ -133,6 +163,10 @@ lemma is_square.div [division_comm_monoid α] {a b : α} (ha : is_square a) (hb 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) :=