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.

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 : α.

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 : α.

theorem isSquare_iff_exists_mul_self {α : Type u_2} [Mul α] (a : α) : IsSquare a ↔ ∃ (r : α), a = r * r

theorem even_iff_exists_add_self {α : Type u_2} [Add α] (a : α) : Even a ↔ ∃ (r : α), a = r + r

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.

theorem Even.exists_add_self {α : Type u_2} [Add α] (a : α) : Even a → ∃ (r : α), a = r + r

@[simp]

theorem IsSquare.mul_self {α : Type u_2} [Mul α] (r : α) : IsSquare (r * r)

@[simp]

theorem Even.add_self {α : Type u_2} [Add α] (r : α) : Even (r + r)

theorem isSquare_op_iff {α : Type u_2} [Mul α] {a : α} : IsSquare (MulOpposite.op a) ↔ IsSquare a

theorem even_op_iff {α : Type u_2} [Add α] {a : α} : Even (AddOpposite.op a) ↔ Even a

theorem isSquare_unop_iff {α : Type u_2} [Mul α] {a : αᵐᵒᵖ} : IsSquare (MulOpposite.unop a) ↔ IsSquare a

theorem even_unop_iff {α : Type u_2} [Add α] {a : αᵃᵒᵖ} : Even (AddOpposite.unop a) ↔ Even a

@[implicit_reducible]

instance instDecidablePredMulOppositeIsSquare {α : Type u_2} [Mul α] [DecidablePred IsSquare] : DecidablePred IsSquare

@[implicit_reducible]

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

@[simp]

theorem even_ofMul_iff {α : Type u_2} [Mul α] {a : α} : Even (Additive.ofMul a) ↔ IsSquare a

@[simp]

theorem isSquare_toMul_iff {α : Type u_2} [Mul α] {a : Additive α} : IsSquare (Additive.toMul a) ↔ Even a

@[implicit_reducible]

instance Additive.instDecidablePredEven {α : Type u_2} [Mul α] [DecidablePred IsSquare] : DecidablePred Even

@[simp]

theorem isSquare_ofAdd_iff {α : Type u_2} [Add α] {a : α} : IsSquare (Multiplicative.ofAdd a) ↔ Even a

@[simp]

theorem even_toAdd_iff {α : Type u_2} [Add α] {a : Multiplicative α} : Even (Multiplicative.toAdd a) ↔ IsSquare a

@[implicit_reducible]

instance Multiplicative.instDecidablePredIsSquare {α : Type u_2} [Add α] [DecidablePred Even] : DecidablePred IsSquare

@[simp]

theorem IsSquare.one {α : Type u_2} [MulOneClass α] : IsSquare 1

@[simp]

theorem Even.zero {α : Type u_2} [AddZeroClass α] : Even 0

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)

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)

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}

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}

theorem isSquare_iff_exists_sq {α : Type u_2} [Monoid α] (a : α) : IsSquare a ↔ ∃ (r : α), a = r ^ 2

theorem even_iff_exists_two_nsmul {α : Type u_2} [AddMonoid α] (a : α) : Even a ↔ ∃ (r : α), a = 2 • r

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.

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.

theorem IsSquare.sq {α : Type u_2} [Monoid α] (r : α) : IsSquare (r ^ 2)

theorem Even.two_nsmul {α : Type u_2} [AddMonoid α] (r : α) : Even (2 • r)

theorem IsSquare.pow {α : Type u_2} [Monoid α] {a : α} (n : ℕ) (ha : IsSquare a) : IsSquare (a ^ n)

theorem Even.nsmul_right {α : Type u_2} [AddMonoid α] {a : α} (n : ℕ) (ha : Even a) : Even (n • a)

theorem Even.isSquare_pow {α : Type u_2} [Monoid α] {n : ℕ} (hn : Even n) (a : α) : IsSquare (a ^ n)

theorem Even.nsmul_left {α : Type u_2} [AddMonoid α] {n : ℕ} (hn : Even n) (a : α) : Even (n • a)

theorem IsSquare.mul {α : Type u_2} [CommSemigroup α] {a b : α} : IsSquare a → IsSquare b → IsSquare (a * b)

theorem Even.add {α : Type u_2} [AddCommSemigroup α] {a b : α} : Even a → Even b → Even (a + b)

@[simp]

theorem isSquare_inv {α : Type u_2} [DivisionMonoid α] {a : α} : IsSquare a⁻¹ ↔ IsSquare a

@[simp]

theorem even_neg {α : Type u_2} [SubtractionMonoid α] {a : α} : Even (-a) ↔ Even a

theorem IsSquare.inv {α : Type u_2} [DivisionMonoid α] {a : α} : IsSquare a → IsSquare a⁻¹

Alias of the reverse direction of isSquare_inv.

theorem Even.neg {α : Type u_2} [SubtractionMonoid α] {a : α} : Even a → Even (-a)

theorem IsSquare.zpow {α : Type u_2} [DivisionMonoid α] {a : α} (n : ℤ) : IsSquare a → IsSquare (a ^ n)

theorem Even.zsmul_right {α : Type u_2} [SubtractionMonoid α] {a : α} (n : ℤ) : Even a → Even (n • a)

theorem IsSquare.div {α : Type u_2} [DivisionCommMonoid α] {a b : α} (ha : IsSquare a) (hb : IsSquare b) : IsSquare (a / b)

theorem Even.sub {α : Type u_2} [SubtractionCommMonoid α] {a b : α} (ha : Even a) (hb : Even b) : Even (a - b)

@[simp]

theorem Even.isSquare_zpow {α : Type u_2} [Group α] {n : ℤ} : Even n → ∀ (a : α), IsSquare (a ^ n)

@[simp]

theorem Even.zsmul_left {α : Type u_2} [AddGroup α] {n : ℤ} : Even n → ∀ (a : α), Even (n • a)