# Squares and even elements #

This file defines square and even elements in a monoid.

## Main declarations #

- `IsSquare a` means that there is some `r` such that `a = r * r`
- `Even a` means that there is some `r` such that `a = r + r`

## Note #

- Many lemmas about `Even` / `IsSquare`, including important `simp` lemmas, are in `Mathlib/Algebra/Ring/Parity.lean`.

## TODO #

- Try to generalize `IsSquare/Even` lemmas further. For example, there are still a few lemmas in `Algebra.Ring.Parity` whose `Semiring` assumptions I (DT) am not convinced are necessary.
- 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.

## See also #

`Mathlib/Algebra/Ring/Parity.lean` for the definition of odd elements as well as facts about `Even` / `IsSquare` in rings.

source
def IsSquare {α : Type u_2} [Mul α] (a : α) :
Prop

An element `a` of a type `α` with multiplication satisfies `IsSquare a` if `a = r * r`, for some root `r : α`.

Equations

- IsSquare a = ∃ (r : α), a = r * r

Instances For

source
def Even {α : Type u_2} [Add α] (a : α) :
Prop

An element `a` of a type `α` with addition satisfies `Even a` if `a = r + r`, for some `r : α`.

Equations

- Even a = ∃ (r : α), a = r + r

Instances For

source
theorem isSquare_iff_exists_mul_self {α : Type u_2} [Mul α] (a : α) :
IsSquare a ↔ ∃ (r : α), a = r * r
source
theorem even_iff_exists_add_self {α : Type u_2} [Add α] (a : α) :
Even a ↔ ∃ (r : α), a = r + r
source
theorem IsSquare.exists_mul_self {α : Type u_2} [Mul α] (a : α) :
IsSquare a → ∃ (r : α), a = r * r

Alias of the forward direction of `isSquare_iff_exists_mul_self`.

source
theorem Even.exists_add_self {α : Type u_2} [Add α] (a : α) :
Even a → ∃ (r : α), a = r + r
source
@[simp]
theorem IsSquare.mul_self {α : Type u_2} [Mul α] (r : α) :
IsSquare (r * r)
source
@[simp]
theorem Even.add_self {α : Type u_2} [Add α] (r : α) :
Even (r + r)
source
theorem isSquare_op_iff {α : Type u_2} [Mul α] {a : α} :
IsSquare (MulOpposite.op a) ↔ IsSquare a
source
theorem even_op_iff {α : Type u_2} [Add α] {a : α} :
Even (AddOpposite.op a) ↔ Even a
source
theorem isSquare_unop_iff {α : Type u_2} [Mul α] {a : α ᵐᵒᵖ} :
IsSquare (MulOpposite.unop a) ↔ IsSquare a
source
theorem even_unop_iff {α : Type u_2} [Add α] {a : α ᵃᵒᵖ} :
Even (AddOpposite.unop a) ↔ Even a
source
instance instDecidablePredMulOppositeIsSquare {α : Type u_2} [Mul α] [DecidablePred IsSquare] :
DecidablePred IsSquare
Equations

- instDecidablePredMulOppositeIsSquare x✝ = decidable_of_iff (IsSquare (MulOpposite.unop x✝)) ⋯

source
instance instDecidablePredAddOppositeEven {α : Type u_2} [Add α] [DecidablePred Even] :
DecidablePred Even
Equations

- instDecidablePredAddOppositeEven x✝ = decidable_of_iff (Even (AddOpposite.unop x✝)) ⋯

source
@[simp]
theorem even_ofMul_iff {α : Type u_2} [Mul α] {a : α} :
Even (Additive.ofMul a) ↔ IsSquare a
source
@[simp]
theorem isSquare_toMul_iff {α : Type u_2} [Mul α] {a : Additive α} :
IsSquare (Additive.toMul a) ↔ Even a
source
instance Additive.instDecidablePredEven {α : Type u_2} [Mul α] [DecidablePred IsSquare] :
DecidablePred Even
Equations

- x✝.instDecidablePredEven = decidable_of_iff (IsSquare (Additive.toMul x✝)) ⋯

source
@[simp]
theorem isSquare_ofAdd_iff {α : Type u_2} [Add α] {a : α} :
IsSquare (Multiplicative.ofAdd a) ↔ Even a
source
@[simp]
theorem even_toAdd_iff {α : Type u_2} [Add α] {a : Multiplicative α} :
Even (Multiplicative.toAdd a) ↔ IsSquare a
source
instance Multiplicative.instDecidablePredIsSquare {α : Type u_2} [Add α] [DecidablePred Even] :
DecidablePred IsSquare
Equations

- x✝.instDecidablePredIsSquare = decidable_of_iff (Even (Multiplicative.toAdd x✝)) ⋯

source
@[simp]
theorem IsSquare.one {α : Type u_2} [MulOneClass α] :
IsSquare 1
source
@[simp]
theorem Even.zero {α : Type u_2} [AddZeroClass α] :
Even 0
source
theorem IsSquare.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] {a : α} (f : F) :
IsSquare a → IsSquare (f a)
source
theorem Even.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddMonoidHomClass F α β] {a : α} (f : F) :
Even a → Even (f a)
source
theorem isSquare_subset_image_isSquare {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] {f : F} (hf : Function.Surjective ⇑f) :
{b : β | IsSquare b} ⊆ ⇑f '' {a : α | IsSquare a}
source
theorem even_subset_image_even {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddMonoidHomClass F α β] {f : F} (hf : Function.Surjective ⇑f) :
{b : β | Even b} ⊆ ⇑f '' {a : α | Even a}
source
theorem isSquare_iff_exists_sq {α : Type u_2} [Monoid α] (a : α) :
IsSquare a ↔ ∃ (r : α), a = r ^ 2
source
theorem even_iff_exists_two_nsmul {α : Type u_2} [AddMonoid α] (a : α) :
Even a ↔ ∃ (r : α), a = 2 • r
source
theorem IsSquare.exists_sq {α : Type u_2} [Monoid α] (a : α) :
IsSquare a → ∃ (r : α), a = r ^ 2

Alias of the forward direction of `isSquare_iff_exists_sq`.

source
theorem Even.exists_two_nsmul {α : Type u_2} [AddMonoid α] (a : α) :
Even a → ∃ (r : α), a = 2 • r

Alias of the forwards direction of `even_iff_exists_two_nsmul`.

source
theorem IsSquare.sq {α : Type u_2} [Monoid α] (r : α) :
IsSquare (r ^ 2)
source
theorem Even.two_nsmul {α : Type u_2} [AddMonoid α] (r : α) :
Even (2 • r)
source
theorem IsSquare.pow {α : Type u_2} [Monoid α] {a : α} (n : ℕ) (ha : IsSquare a) :
IsSquare (a ^ n)
source
theorem Even.nsmul_right {α : Type u_2} [AddMonoid α] {a : α} (n : ℕ) (ha : Even a) :
Even (n • a)
source
theorem Even.isSquare_pow {α : Type u_2} [Monoid α] {n : ℕ} (hn : Even n) (a : α) :
IsSquare (a ^ n)
source
theorem Even.nsmul_left {α : Type u_2} [AddMonoid α] {n : ℕ} (hn : Even n) (a : α) :
Even (n • a)
source
theorem IsSquare.mul {α : Type u_2} [CommSemigroup α] {a b : α} :
IsSquare a → IsSquare b → IsSquare (a * b)
source
theorem Even.add {α : Type u_2} [AddCommSemigroup α] {a b : α} :
Even a → Even b → Even (a + b)
source
@[simp]
theorem isSquare_inv {α : Type u_2} [DivisionMonoid α] {a : α} :
IsSquare a⁻¹ ↔ IsSquare a
source
@[simp]
theorem even_neg {α : Type u_2} [SubtractionMonoid α] {a : α} :
Even (-a) ↔ Even a
source
theorem IsSquare.inv {α : Type u_2} [DivisionMonoid α] {a : α} :
IsSquare a → IsSquare a⁻¹

Alias of the reverse direction of `isSquare_inv`.

source
theorem Even.neg {α : Type u_2} [SubtractionMonoid α] {a : α} :
Even a → Even (-a)
source
theorem IsSquare.zpow {α : Type u_2} [DivisionMonoid α] {a : α} (n : ℤ) :
IsSquare a → IsSquare (a ^ n)
source
theorem Even.zsmul_right {α : Type u_2} [SubtractionMonoid α] {a : α} (n : ℤ) :
Even a → Even (n • a)
source
theorem IsSquare.div {α : Type u_2} [DivisionCommMonoid α] {a b : α} (ha : IsSquare a) (hb : IsSquare b) :
IsSquare (a / b)
source
theorem Even.sub {α : Type u_2} [SubtractionCommMonoid α] {a b : α} (ha : Even a) (hb : Even b) :
Even (a - b)
source
@[simp]
theorem Even.isSquare_zpow {α : Type u_2} [Group α] {n : ℤ} :
Even n → ∀ (a : α), IsSquare (a ^ n)
source
@[simp]
theorem Even.zsmul_left {α : Type u_2} [AddGroup α] {n : ℤ} :
Even n → ∀ (a : α), Even (n • a)