doc-next-gen

Mathlib.Algebra.Group.Even

Module docstring

{"# 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.

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 as well as facts about Even / IsSquare in rings. "}

IsSquare definition
(a : α) : Prop
Full source 
/-- An element `a` of a type `α` with multiplication satisfies `IsSquare a` if `a = r * r`,
for some root `r : α`. -/
@[to_additive "An element `a` of a type `α` with addition satisfies `Even a` if `a = r + r`,
for some `r : α`."]
def IsSquare (a : α) : Prop := ∃ r, a = r * r
Square element in a multiplicative monoid
Informal description
An element $a$ of a type $\alpha$ with multiplication is called a *square* if there exists an element $r \in \alpha$ such that $a = r \cdot r$.
IsSquare.mul_self theorem
(r : α) : IsSquare (r * r)
Full source 
@[to_additive (attr := simp)] lemma IsSquare.mul_self (r : α) : IsSquare (r * r) := ⟨r, rfl⟩
Square of an Element is a Square
Informal description
For any element $r$ in a multiplicative monoid $\alpha$, the product $r \cdot r$ is a square element in $\alpha$.
isSquare_op_iff theorem
{a : α} : IsSquare (op a) ↔ IsSquare a
Full source 
@[to_additive]
lemma isSquare_op_iff {a : α} : IsSquareIsSquare (op a) ↔ IsSquare a :=
  ⟨fun ⟨r, hr⟩ ↦ ⟨unop r, congr_arg unop hr⟩, fun ⟨r, hr⟩ ↦ ⟨op r, congr_arg op hr⟩⟩
Square Elements in Multiplicative Opposite iff Square in Original Monoid
Informal description
For any element $a$ in a multiplicative monoid $\alpha$, the element $\text{op}(a)$ in the multiplicative opposite $\alpha^\text{op}$ is a square if and only if $a$ is a square in $\alpha$.
isSquare_unop_iff theorem
{a : αᵐᵒᵖ} : IsSquare (unop a) ↔ IsSquare a
Full source 
@[to_additive]
lemma isSquare_unop_iff {a : αᵐᵒᵖ} : IsSquareIsSquare (unop a) ↔ IsSquare a := isSquare_op_iff.symm
Square Elements in Original Monoid iff Square in Multiplicative Opposite
Informal description
For any element $a$ in the multiplicative opposite $\alpha^\text{op}$ of a monoid $\alpha$, the element $\text{unop}(a)$ is a square in $\alpha$ if and only if $a$ is a square in $\alpha^\text{op}$.
instDecidablePredMulOppositeIsSquare instance
[DecidablePred (IsSquare : α → Prop)] : DecidablePred (IsSquare : αᵐᵒᵖ → Prop)
Full source 
@[to_additive]
instance [DecidablePred (IsSquare : α → Prop)] : DecidablePred (IsSquare : αᵐᵒᵖ → Prop) :=
  fun _ ↦ decidable_of_iff _ isSquare_unop_iff
Decidability of Square Elements in Multiplicative Opposite
Informal description
For any type $\alpha$ with a decidable predicate `IsSquare`, the multiplicative opposite $\alpha^\text{op}$ also has a decidable `IsSquare` predicate.
even_ofMul_iff theorem
{a : α} : Even (Additive.ofMul a) ↔ IsSquare a
Full source 
@[simp]
lemma even_ofMul_iff {a : α} : EvenEven (Additive.ofMul a) ↔ IsSquare a := Iff.rfl
Equivalence between Evenness in Additive Monoid and Squareness in Multiplicative Monoid
Informal description
For any element $a$ in a multiplicative monoid $\alpha$, the element $\text{Additive.ofMul}(a)$ is even (i.e., can be written as $r + r$ for some $r$) if and only if $a$ is a square (i.e., can be written as $r \cdot r$ for some $r$).
isSquare_toMul_iff theorem
{a : Additive α} : IsSquare (a.toMul) ↔ Even a
Full source 
@[simp]
lemma isSquare_toMul_iff {a : Additive α} : IsSquareIsSquare (a.toMul) ↔ Even a := Iff.rfl
Squareness of Multiplicative Element Equivalent to Evenness in Additive Monoid
Informal description
For any element $a$ in the additive monoid $\alpha$, the multiplicative version of $a$ (denoted as $a^\mathrm{toMul}$) is a square in the multiplicative monoid if and only if $a$ is even in the additive monoid, i.e., there exists an element $r$ such that $a = r + r$.
Additive.instDecidablePredEven instance
[DecidablePred (IsSquare : α → Prop)] : DecidablePred (Even : Additive α → Prop)
Full source 
instance Additive.instDecidablePredEven [DecidablePred (IsSquare : α → Prop)] :
    DecidablePred (Even : Additive α → Prop) :=
  fun _ ↦ decidable_of_iff _ isSquare_toMul_iff
Decidability of Even Elements in Additive Monoid from Square Elements
Informal description
For any type $\alpha$ with a decidable predicate on square elements, the additive monoid of $\alpha$ has a decidable predicate on even elements. That is, given a way to decide whether an element of $\alpha$ is a square (i.e., of the form $r \cdot r$), we can decide whether an element of the additive monoid is even (i.e., of the form $r + r$).
isSquare_ofAdd_iff theorem
{a : α} : IsSquare (Multiplicative.ofAdd a) ↔ Even a
Full source 
@[simp] lemma isSquare_ofAdd_iff {a : α} : IsSquareIsSquare (Multiplicative.ofAdd a) ↔ Even a := Iff.rfl
Square of Additive-to-Multiplicative Element iff Even in Additive Monoid
Informal description
For any element $a$ of type $\alpha$, the element $\text{Multiplicative.ofAdd}(a)$ is a square in the multiplicative monoid if and only if $a$ is even in the additive monoid (i.e., there exists an element $r$ such that $a = r + r$).
even_toAdd_iff theorem
{a : Multiplicative α} : Even a.toAdd ↔ IsSquare a
Full source 
@[simp]
lemma even_toAdd_iff {a : Multiplicative α} : EvenEven a.toAdd ↔ IsSquare a := Iff.rfl
Equivalence Between Evenness in Additive Monoid and Squareness in Multiplicative Monoid
Informal description
For any element $a$ in the multiplicative monoid of type $\alpha$, the additive version of $a$ (denoted as $a.\text{toAdd}$) is even if and only if $a$ is a square in the multiplicative monoid. That is, there exists an element $r$ such that $a.\text{toAdd} = r + r$ if and only if there exists an element $s$ such that $a = s \cdot s$.
Multiplicative.instDecidablePredIsSquare instance
[DecidablePred (Even : α → Prop)] : DecidablePred (IsSquare : Multiplicative α → Prop)
Full source 
instance Multiplicative.instDecidablePredIsSquare [DecidablePred (Even : α → Prop)] :
    DecidablePred (IsSquare : Multiplicative α → Prop) :=
  fun _ ↦ decidable_of_iff _ even_toAdd_iff
Decidability of Square Elements in Multiplicative Monoid from Even Elements in Additive Monoid
Informal description
For any type $\alpha$ with a decidable predicate on even elements, the multiplicative monoid of $\alpha$ has a decidable predicate on square elements.
IsSquare.one theorem
[MulOneClass α] : IsSquare (1 : α)
Full source 
@[to_additive (attr := simp)]
lemma IsSquare.one [MulOneClass α] : IsSquare (1 : α) := ⟨1, (mul_one _).symm⟩
The identity element is a square in a monoid
Informal description
In any multiplicative monoid $\alpha$ with identity element $1$, the element $1$ is a square, i.e., there exists an element $r \in \alpha$ such that $1 = r \cdot r$.
IsSquare.map theorem
{a : α} (f : F) : IsSquare a → IsSquare (f a)
Full source 
@[to_additive]
lemma IsSquare.map {a : α} (f : F) : IsSquare a → IsSquare (f a) :=
  fun ⟨r, _⟩ => ⟨f r, by simp_all⟩
Preservation of Square Elements under Monoid Homomorphisms
Informal description
Let $F$ be a type of homomorphisms between monoids that preserve multiplication and the identity element. For any element $a$ in a monoid $\alpha$, if $a$ is a square (i.e., there exists $r \in \alpha$ such that $a = r \cdot r$), then its image $f(a)$ under any homomorphism $f \in F$ is also a square in the codomain monoid.
IsSquare.sq theorem
(r : α) : IsSquare (r ^ 2)
Full source 
@[to_additive Even.two_nsmul]
lemma IsSquare.sq (r : α) : IsSquare (r ^ 2) := ⟨r, pow_two _⟩
Square of an Element is a Square Element
Informal description
For any element $r$ in a monoid $\alpha$, the square $r^2$ is a square element, i.e., there exists an element $s \in \alpha$ such that $r^2 = s \cdot s$.
IsSquare.pow theorem
(n : ℕ) : IsSquare a → IsSquare (a ^ n)
Full source 
@[to_additive Even.nsmul_right] lemma IsSquare.pow (n : ℕ) : IsSquare a → IsSquare (a ^ n) := by
  rintro ⟨r, rfl⟩; exact ⟨r ^ n, (Commute.refl _).mul_pow _⟩
Power of a Square Element is Square
Informal description
For any natural number $n$ and any element $a$ in a monoid $\alpha$, if $a$ is a square (i.e., there exists $r \in \alpha$ such that $a = r \cdot r$), then $a^n$ is also a square.
Even.isSquare_pow theorem
: Even n → ∀ a : α, IsSquare (a ^ n)
Full source 
@[to_additive (attr := simp) Even.nsmul_left]
lemma Even.isSquare_pow : Even n → ∀ a : α, IsSquare (a ^ n) := by
  rintro ⟨m, rfl⟩ a; exact ⟨a ^ m, pow_add _ _ _⟩
Even Powers are Squares in a Monoid
Informal description
For any natural number $n$ and any element $a$ in a monoid $\alpha$, if $n$ is even (i.e., there exists $k \in \mathbb{N}$ such that $n = 2k$), then $a^n$ is a square (i.e., there exists $r \in \alpha$ such that $a^n = r \cdot r$).
IsSquare.mul theorem
[CommSemigroup α] {a b : α} : IsSquare a → IsSquare b → IsSquare (a * b)
Full source 
@[to_additive]
lemma IsSquare.mul [CommSemigroup α] {a b : α} : IsSquare a → IsSquare b → IsSquare (a * b) := by
  rintro ⟨r, rfl⟩ ⟨s, rfl⟩; exact ⟨r * s, mul_mul_mul_comm _ _ _ _⟩
Product of Squares is Square in a Commutative Semigroup
Informal description
Let $\alpha$ be a commutative semigroup. For any elements $a, b \in \alpha$, if both $a$ and $b$ are squares (i.e., there exist $r, s \in \alpha$ such that $a = r \cdot r$ and $b = s \cdot s$), then their product $a \cdot b$ is also a square.
isSquare_inv theorem
: IsSquare a⁻¹ ↔ IsSquare a
Full source 
@[to_additive (attr := simp)] lemma isSquare_inv : IsSquareIsSquare a⁻¹ ↔ IsSquare a := by
  constructor <;> intro h <;> simpa using (isSquare_op_iff.mpr h).map (MulEquiv.inv' α).symm
Square Elements and Their Inverses: $a^{-1}$ is square iff $a$ is square
Informal description
For any element $a$ in a division monoid $\alpha$, the inverse $a^{-1}$ is a square if and only if $a$ itself is a square. That is, there exists an element $r \in \alpha$ such that $a^{-1} = r \cdot r$ if and only if there exists an element $s \in \alpha$ such that $a = s \cdot s$.
IsSquare.zpow theorem
(n : ℤ) : IsSquare a → IsSquare (a ^ n)
Full source 
@[to_additive Even.zsmul_right] lemma IsSquare.zpow (n : ℤ) : IsSquare a → IsSquare (a ^ n) := by
  rintro ⟨r, rfl⟩; exact ⟨r ^ n, (Commute.refl _).mul_zpow _⟩
Integer Powers Preserve Square Elements in Division Monoids
Informal description
Let $\alpha$ be a division monoid and let $a \in \alpha$ be a square element (i.e., there exists $r \in \alpha$ such that $a = r \cdot r$). Then for any integer $n$, the element $a^n$ is also a square.
IsSquare.div theorem
[DivisionCommMonoid α] {a b : α} (ha : IsSquare a) (hb : IsSquare b) : IsSquare (a / b)
Full source 
@[to_additive]
lemma IsSquare.div [DivisionCommMonoid α] {a b : α} (ha : IsSquare a) (hb : IsSquare b) :
    IsSquare (a / b) := by rw [div_eq_mul_inv]; exact ha.mul hb.inv
Quotient of Squares is Square in a Commutative Division Monoid
Informal description
Let $\alpha$ be a commutative division monoid. For any elements $a, b \in \alpha$, if both $a$ and $b$ are squares (i.e., there exist $r, s \in \alpha$ such that $a = r^2$ and $b = s^2$), then their quotient $a / b$ is also a square.
Even.isSquare_zpow theorem
[Group α] {n : ℤ} : Even n → ∀ a : α, IsSquare (a ^ n)
Full source 
@[to_additive (attr := simp) Even.zsmul_left]
lemma Even.isSquare_zpow [Group α] {n : ℤ} : Even n → ∀ a : α, IsSquare (a ^ n) := by
  rintro ⟨m, rfl⟩ a; exact ⟨a ^ m, zpow_add _ _ _⟩
Even Powers are Squares in a Group: $a^n$ is square when $n$ is even
Informal description
Let $\alpha$ be a group and $n$ be an integer. If $n$ is even, then for every element $a \in \alpha$, the power $a^n$ is a square in $\alpha$, i.e., there exists an element $r \in \alpha$ such that $a^n = r \cdot r$.