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.

Mathlib.Algebra.Ring.Parity for the definition of odd elements.

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

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

Equations
Instances For
def IsSquare {α : Type u_2} [Mul α] (a : α) :

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

Equations
• = ∃ (r : α), a = r * r
Instances For
@[simp]
theorem even_add_self {α : Type u_2} [Add α] (m : α) :
Even (m + m)
@[simp]
theorem isSquare_mul_self {α : Type u_2} [Mul α] (m : α) :
IsSquare (m * m)
theorem even_op_iff {α : Type u_2} [Add α] {a : α} :
theorem isSquare_op_iff {α : Type u_2} [Mul α] {a : α} :
theorem even_unop_iff {α : Type u_2} [Add α] {a : αᵃᵒᵖ} :
theorem isSquare_unop_iff {α : Type u_2} [Mul α] {a : αᵐᵒᵖ} :
Equations
instance instDecidablePredMulOppositeIsSquare {α : Type u_2} [Mul α] [DecidablePred IsSquare] :
DecidablePred IsSquare
Equations
@[simp]
theorem even_ofMul_iff {α : Type u_2} [Mul α] {a : α} :
@[simp]
theorem isSquare_toMul_iff {α : Type u_2} [Mul α] {a : } :
instance Additive.instDecidablePredEven {α : Type u_2} [Mul α] [DecidablePred IsSquare] :
Equations
@[simp]
theorem isSquare_ofAdd_iff {α : Type u_2} [Add α] {a : α} :
@[simp]
theorem even_toAdd_iff {α : Type u_2} [Add α] {a : } :
Equations
@[simp]
theorem even_zero {α : Type u_2} [] :
@[simp]
theorem isSquare_one {α : Type u_2} [] :
theorem Even.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] {m : α} (f : F) :
Even mEven (f m)
theorem IsSquare.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] {m : α} (f : F) :
IsSquare (f m)
theorem even_iff_exists_two_nsmul {α : Type u_2} [] (m : α) :
Even m ∃ (c : α), m = 2 c
theorem isSquare_iff_exists_sq {α : Type u_2} [] (m : α) :
∃ (c : α), m = c ^ 2
theorem IsSquare.exists_sq {α : Type u_2} [] (m : α) :
∃ (c : α), m = c ^ 2

Alias of the forward direction of isSquare_iff_exists_sq.

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

Alias of the reverse direction of isSquare_iff_exists_sq.

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

Alias of the forwards direction of even_iff_exists_two_nsmul.

theorem Even.nsmul {α : Type u_2} [] {a : α} (n : ) :
Even aEven (n a)
theorem IsSquare.pow {α : Type u_2} [] {a : α} (n : ) :
IsSquare (a ^ n)
theorem Even.nsmul' {α : Type u_2} [] {n : } :
Even n∀ (a : α), Even (n a)
theorem Even.isSquare_pow {α : Type u_2} [] {n : } :
Even n∀ (a : α), IsSquare (a ^ n)
theorem even_two_nsmul {α : Type u_2} [] (a : α) :
Even (2 a)
theorem IsSquare_sq {α : Type u_2} [] (a : α) :
IsSquare (a ^ 2)
theorem Even.add {α : Type u_2} [] {a : α} {b : α} :
Even aEven bEven (a + b)
theorem IsSquare.mul {α : Type u_2} [] {a : α} {b : α} :
IsSquare (a * b)
@[simp]
theorem even_neg {α : Type u_2} {a : α} :
Even (-a) Even a
@[simp]
theorem isSquare_inv {α : Type u_2} [] {a : α} :
theorem IsSquare.inv {α : Type u_2} [] {a : α} :

Alias of the reverse direction of isSquare_inv.

theorem Even.neg {α : Type u_2} {a : α} :
Even aEven (-a)
theorem Even.zsmul {α : Type u_2} {a : α} (n : ) :
Even aEven (n a)
theorem IsSquare.zpow {α : Type u_2} [] {a : α} (n : ) :
IsSquare (a ^ n)
theorem Even.sub {α : Type u_2} {a : α} {b : α} (ha : Even a) (hb : Even b) :
Even (a - b)
theorem IsSquare.div {α : Type u_2} {a : α} {b : α} (ha : ) (hb : ) :
IsSquare (a / b)
@[simp]
theorem Even.zsmul' {α : Type u_2} [] {n : } :
Even n∀ (a : α), Even (n a)
@[simp]
theorem Even.isSquare_zpow {α : Type u_2} [] {n : } :
Even n∀ (a : α), IsSquare (a ^ n)