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

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 for the definition of odd elements.

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

Equations

• IsSquare a = ∃ (r : α), a = r * 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 : α.

Equations

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

@[simp]

theorem isSquare_mul_self {α : Type u_2} [Mul α] (m : α) : IsSquare (m * m)

@[simp]

theorem even_add_self {α : Type u_2} [Add α] (m : α) : Even (m + m)

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

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

Equations

• instDecidablePredMulOppositeIsSquare x = decidable_of_iff (IsSquare (MulOpposite.unop x)) ⋯

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

Equations

• instDecidablePredAddOppositeEven x = decidable_of_iff (Even (AddOpposite.unop x)) ⋯

@[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

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

Equations

• x.instDecidablePredEven = decidable_of_iff (IsSquare (Additive.toMul x)) ⋯

@[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

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

Equations

• x.instDecidablePredIsSquare = decidable_of_iff (Even (Multiplicative.toAdd x)) ⋯

@[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 α β] {m : α} (f : F) : IsSquare m → IsSquare (f m)

theorem Even.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddMonoidHomClass F α β] {m : α} (f : F) : Even m → Even (f m)

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

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

theorem IsSquare.exists_sq {α : Type u_2} [Monoid α] (m : α) : IsSquare m → ∃ (c : α), m = c ^ 2

Alias of the forward direction of isSquare_iff_exists_sq.

theorem isSquare_of_exists_sq {α : Type u_2} [Monoid α] (m : α) : (∃ (c : α), m = c ^ 2) → IsSquare m

Alias of the reverse direction of isSquare_iff_exists_sq.

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

Alias of the forwards direction of even_iff_exists_two_nsmul.

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

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

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

theorem Even.nsmul' {α : Type u_2} [AddMonoid α] {n : ℕ} : Even n → ∀ (a : α), Even (n • a)

theorem IsSquare_sq {α : Type u_2} [Monoid α] (a : α) : IsSquare (a ^ 2)

theorem even_two_nsmul {α : Type u_2} [AddMonoid α] (a : α) : Even (2 • 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 {α : 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' {α : Type u_2} [AddGroup α] {n : ℤ} : Even n → ∀ (a : α), Even (n • a)