Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2022 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
! This file was ported from Lean 3 source module algebra.parity
! leanprover-community/mathlib commit 8631e2d5ea77f6c13054d9151d82b83069680cb1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GroupPower.Lemmas
import Mathlib.Data.Nat.Cast.Basic
/-! # Squares, even and odd elements
This file proves some general facts about squares, even and odd elements of semirings.
In the implementation, we define `IsSquare` and we let `Even` be the notion transported by
`to_additive`. The definition are therefore as follows:
```lean
IsSquare a ↔ ∃ r, a = r * r
Even a ↔ ∃ r, a = r + r
```
Odd elements are not unified with a multiplicative notion.
## Future work
* TODO: Try to generalize further the typeclass assumptions on `IsSquare/Even`.
For instance, in some cases, there are `Semiring` assumptions that I (DT) am not convinced are
necessary.
* TODO: Consider moving the definition and lemmas about `Odd` to a separate file.
* TODO: 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.
-/
open MulOpposite
variable { F α β R : Type _ }
section Mul
variable [ Mul α ]
/-- An element `a` of a type `α` with multiplication satisfies `IsSquare a` if `a = r * r`,
for some `r : α`. -/
@[ to_additive : {α : Type u_1} → [inst : Add α α → Prop 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
#align is_square IsSquare
#align even Even
@[ to_additive : ∀ {α : Type u_1} [inst : Add α m : α ), Even (m + m to_additive ( attr := simp )]
theorem isSquare_mul_self : ∀ (m : α ), IsSquare (m * m isSquare_mul_self ( m : α ) : IsSquare : {α : Type ?u.151} → [inst : Mul α α → Prop ( m * m ) :=
⟨ m , rfl : ∀ {α : Sort ?u.249} {a : α }, a = a ⟩
#align is_square_mul_self isSquare_mul_self
#align even_add_self even_add_self : ∀ {α : Type u_1} [inst : Add α m : α ), Even (m + m
@[ to_additive ]
theorem isSquare_op_iff ( a : α ) : IsSquare : {α : Type ?u.328} → [inst : Mul α α → Prop ( op a ) ↔ IsSquare : {α : Type ?u.356} → [inst : Mul α α → Prop a :=
⟨ fun ⟨ c , hc ⟩ => ⟨ unop c , by rw [ ← unop_mul , ← hc , unop_op ] ⟩, fun ⟨ c , hc ⟩ => by simp [ hc ] ⟩
#align is_square_op_iff isSquare_op_iff
#align even_op_iff even_op_iff
end Mul
@[ to_additive ( attr := simp )]
theorem isSquare_one [ MulOneClass α ] : IsSquare : {α : Type ?u.891} → [inst : Mul α α → Prop ( 1 : α ) :=
⟨ 1 , ( mul_one _ ). symm : ∀ {α : Sort ?u.2140} {a b : α }, a = b b = a symm ⟩
#align is_square_one isSquare_one
#align even_zero even_zero
@[ to_additive ]
theorem IsSquare.map [ MulOneClass : Type ?u.2221 → Type ?u.2221 α ] [ MulOneClass : Type ?u.2224 → Type ?u.2224 β ] [ MonoidHomClass F α β ] { m : α } ( f : F ) :
IsSquare : {α : Type ?u.2249} → [inst : Mul α α → Prop m → IsSquare : {α : Type ?u.2588} → [inst : Mul α α → Prop ( f m ) := by
rintro ⟨ m , rfl ⟩
exact ⟨ f m , by simp ⟩
#align is_square.map IsSquare.map
#align even.map Even.map
section Monoid
variable [ Monoid α ] { n : ℕ } { a : α }
@[ to_additive even_iff_exists_two_nsmul ]
theorem isSquare_iff_exists_sq ( m : α ) : IsSquare : {α : Type ?u.5189} → [inst : Mul α α → Prop m ↔ ∃ c , m = c ^ 2 := by simp [ IsSquare : {α : Type ?u.5667} → [inst : Mul α α → Prop , pow_two : ∀ {M : Type ?u.5678} [inst : Monoid M a : M ), a ^ 2 = a * a ]
#align is_square_iff_exists_sq isSquare_iff_exists_sq
#align even_iff_exists_two_nsmul even_iff_exists_two_nsmul
alias isSquare_iff_exists_sq ↔ IsSquare.exists_sq isSquare_of_exists_sq
#align is_square.exists_sq IsSquare.exists_sq
#align is_square_of_exists_sq isSquare_of_exists_sq
attribute
[ to_additive Even.exists_two_nsmul
"Alias of the forwards direction of `even_iff_exists_two_nsmul`."]
IsSquare.exists_sq
#align even.exists_two_nsmul Even.exists_two_nsmul
@[ to_additive ]
theorem IsSquare.pow ( n : ℕ ) : IsSquare : {α : Type ?u.8168} → [inst : Mul α α → Prop a → IsSquare : {α : Type ?u.8520} → [inst : Mul α α → Prop ( a ^ n ) := by
rintro ⟨ a , rfl ⟩
exact ⟨ a ^ n , ( Commute.refl : ∀ {S : Type ?u.13654} [inst : Mul S a : S ), Commute a a _ ). mul_pow _ ⟩
#align is_square.pow IsSquare.pow
#align even.nsmul Even.nsmul
/- Porting note: `simp` attribute removed because linter reports:
simp can prove this:
by simp only [even_two, Even.nsmul']
-/
@[ to_additive Even.nsmul' ]
theorem Even.isSquare_pow : Even n → ∀ a : α , IsSquare : {α : Type ?u.14125} → [inst : Mul α α → Prop ( a ^ n ) := by
rintro ⟨ n , rfl ⟩ a
exact ⟨ a ^ n , pow_add : ∀ {M : Type ?u.19594} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m + n = a ^ m * a ^ n _ _ _ ⟩
#align even.is_square_pow Even.isSquare_pow
#align even.nsmul' Even.nsmul'
/- Porting note: `simp` attribute removed because linter reports:
simp can prove this:
by simp only [even_two, Even.is_square_pow]
-/
@[ to_additive even_two_nsmul ]
theorem IsSquare_sq ( a : α ) : IsSquare : {α : Type ?u.19705} → [inst : Mul α α → Prop ( a ^ 2 ) :=
⟨ a , pow_two : ∀ {M : Type ?u.20303} [inst : Monoid M a : M ), a ^ 2 = a * a _ ⟩
#align is_square_sq IsSquare_sq
#align even_two_nsmul even_two_nsmul
variable [ HasDistribNeg : (α : Type ?u.24643) → [inst : Mul α Type ?u.24643 α ]
theorem Even.neg_pow : Even n ∀ (a : α ), (- a ^ n = a ^ n Even.neg_pow : Even n → ∀ a : α , (- a ) ^ n = a ^ n := by
rintro ⟨ c , rfl ⟩ a
simp_rw [ ← two_mul , pow_mul : ∀ {M : Type ?u.24475} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m * n = (a ^ m ^ n , neg_sq ]
#align even.neg_pow Even.neg_pow
theorem Even.neg_one_pow ( h : Even n ) : (- 1 : α ) ^ n = 1 := by rw [ h . neg_pow , one_pow : ∀ {M : Type ?u.28406} [inst : Monoid M n : ℕ ), 1 ^ n = 1 ]
#align even.neg_one_pow Even.neg_one_pow
end Monoid
@[ to_additive ]
theorem IsSquare.mul [ CommSemigroup : Type ?u.28476 → Type ?u.28476 α ] { a b : α } : IsSquare : {α : Type ?u.28484} → [inst : Mul α α → Prop a → IsSquare : {α : Type ?u.29035} → [inst : Mul α α → Prop b → IsSquare : {α : Type ?u.29062} → [inst : Mul α α → Prop ( a * b ) := by
rintro ⟨ a , rfl ⟩ ⟨ b , rfl ⟩
exact ⟨ a * b , mul_mul_mul_comm _ _ _ _ ⟩
#align is_square.mul IsSquare.mul
#align even.add Even.add
variable ( α )
@[ simp ]
theorem isSquare_zero [ MulZeroClass : Type ?u.31094 → Type ?u.31094 α ] : IsSquare : {α : Type ?u.31097} → [inst : Mul α α → Prop ( 0 : α ) :=
⟨ 0 , ( mul_zero _ ). symm : ∀ {α : Sort ?u.31927} {a b : α }, a = b b = a symm ⟩
#align is_square_zero isSquare_zero
variable { α }
section DivisionMonoid
variable [ DivisionMonoid : Type ?u.34445 → Type ?u.34445 α ] { a : α }
@[ to_additive ( attr := simp )]
theorem isSquare_inv : IsSquare : {α : Type ?u.32022} → [inst : Mul α α → Prop a ⁻¹ ↔ IsSquare : {α : Type ?u.32447} → [inst : Mul α α → Prop a := by
refine' ⟨ fun h => _ , fun h => _ ⟩
· rw [ ← isSquare_op_iff , ← inv_inv a ]
exact h . map ( MulEquiv.inv' α )
· exact (( isSquare_op_iff a ). mpr : ∀ {a b : Prop }, (a ↔ b b → a mpr h ). map ( MulEquiv.inv' α ). symm : {M : Type ?u.33730} → {N : Type ?u.33729} → [inst : Mul M [inst_1 : Mul N M ≃* N N ≃* M symm
#align is_square_inv isSquare_inv
#align even_neg even_neg
alias isSquare_inv ↔ _ IsSquare.inv
#align is_square.inv IsSquare.inv
attribute [ to_additive ] IsSquare.inv
#align even.neg Even.neg
@[ to_additive ]
theorem IsSquare.zpow ( n : ℤ ) : IsSquare : {α : Type ?u.34453} → [inst : Mul α α → Prop a → IsSquare : {α : Type ?u.34841} → [inst : Mul α α → Prop ( a ^ n ) := by
rintro ⟨ a , rfl ⟩
exact ⟨ a ^ n , ( Commute.refl : ∀ {S : Type ?u.40133} [inst : Mul S a : S ), Commute a a _ ). mul_zpow _ ⟩
#align is_square.zpow IsSquare.zpow
#align even.zsmul Even.zsmul
variable [ HasDistribNeg : (α : Type ?u.44669) → [inst : Mul α Type ?u.44669 α ] { n : ℤ }
theorem Even.neg_zpow : Even n ∀ (a : α ), (- a ^ n = a ^ n Even.neg_zpow : Even n → ∀ a : α , (- a ) ^ n = a ^ n := by
rintro ⟨ c , rfl ⟩ a
exact zpow_bit0_neg _ _
#align even.neg_zpow Even.neg_zpow
theorem Even.neg_one_zpow ( h : Even n ) : (- 1 : α ) ^ n = 1 := by rw [ h . neg_zpow , one_zpow ]
#align even.neg_one_zpow Even.neg_one_zpow
end DivisionMonoid
theorem even_abs [ SubtractionMonoid : Type ?u.48538 → Type ?u.48538 α ] [ LinearOrder : Type ?u.48541 → Type ?u.48541 α ] { a : α } : Even (| a |) ↔ Even a := by
cases abs_choice a
· have h : abs : {α : Type ?u.49263} → [self : Abs α α → α a = a := by assumption
simp only [ h , even_neg ]
· have h : abs : {α : Type ?u.49573} → [self : Abs α α → α a = - a := by assumption
simp only [ h , even_neg ]
#align even_abs even_abs
@[ to_additive ]
theorem IsSquare.div [ DivisionCommMonoid : Type ?u.49659 → Type ?u.49659 α ] { a b : α } ( ha : IsSquare : {α : Type ?u.49666} → [inst : Mul α α → Prop a ) ( hb : IsSquare : {α : Type ?u.50061} → [inst : Mul α α → Prop b ) :
IsSquare : {α : Type ?u.50089} → [inst : Mul α α → Prop ( a / b ) := by
rw [ div_eq_mul_inv ]
exact ha . mul hb . inv
#align is_square.div IsSquare.div
#align even.sub Even.sub
@[ to_additive ( attr := simp ) Even.zsmul' ]
theorem Even.isSquare_zpow [ Group α ] { n : ℤ } : Even n → ∀ a : α , IsSquare : {α : Type ?u.50666} → [inst : Mul α α → Prop ( a ^ n ) := by
rintro ⟨ n , rfl ⟩ a
exact ⟨ a ^ n , zpow_add : ∀ {G : Type ?u.56286} [inst : Group G a : G ) (m n : ℤ ), a ^ (m + n = a ^ m * a ^ n _ _ _ ⟩
#align even.is_square_zpow Even.isSquare_zpow
#align even.zsmul' Even.zsmul'
-- `Odd.tsub` requires `CanonicallyLinearOrderedSemiring`, which we don't have
theorem Even.tsub [ CanonicallyLinearOrderedAddMonoid : Type ?u.56426 → Type ?u.56426 α ] [ Sub α ] [ OrderedSub : (α : Type ?u.56432) → [inst : LE α [inst : Add α [inst : Sub α Prop α ]
[ ContravariantClass : (M : Type ?u.57051) → (N : Type ?u.57050) → (M → N → N (N → N → Prop Prop α α (· + ·) (· ≤ ·) ] { m n : α } ( hm : Even m ) ( hn : Even n ) :
Even ( m - n ) := by
obtain ⟨ a , rfl ⟩ := hm
obtain ⟨ b , rfl ⟩ := hn
refine' ⟨ a - b , _ ⟩
obtain h | h := le_total a b intro.intro.inl intro.intro.inr
· intro.intro.inl intro.intro.inr rw [ tsub_eq_zero_of_le h , tsub_eq_zero_of_le ( add_le_add h h ), add_zero ]
· exact ( tsub_add_tsub_comm h h ). symm : ∀ {α : Sort ?u.60307} {a b : α }, a = b b = a symm
#align even.tsub Even.tsub
set_option linter.deprecated false in
theorem even_iff_exists_bit0 : ∀ [inst : Add α a : α }, Even a ↔ ∃ b , a = bit0 b even_iff_exists_bit0 [ Add α ] { a : α } : Even a ↔ ∃ b , a = bit0 : {α : Type ?u.60385} → [inst : Add α α → α b :=
Iff.rfl : ∀ {a : Prop }, a ↔ a
#align even_iff_exists_bit0 even_iff_exists_bit0 : ∀ {α : Type u_1} [inst : Add α a : α }, Even a ↔ ∃ b , a = bit0 b
alias even_iff_exists_bit0 : ∀ {α : Type u_1} [inst : Add α a : α }, Even a ↔ ∃ b , a = bit0 b ↔ Even.exists_bit0 : ∀ {α : Type u_1} [inst : Add α a : α }, Even a ∃ b , a = bit0 b _
#align even.exists_bit0 Even.exists_bit0 : ∀ {α : Type u_1} [inst : Add α a : α }, Even a ∃ b , a = bit0 b
section Semiring
variable [ Semiring α ] [ Semiring β ] { m n : α }
theorem even_iff_exists_two_mul ( m : α ) : Even m ↔ ∃ c , m = 2 * c := by
simp [ even_iff_exists_two_nsmul : ∀ {α : Type ?u.60871} [inst : AddMonoid α m : α ), Even m ↔ ∃ c , m = 2 • c ]
#align even_iff_exists_two_mul even_iff_exists_two_mul
theorem even_iff_two_dvd { a : α } : Even a ↔ 2 ∣ a := by simp [ Even , Dvd.dvd : {α : Type ?u.63740} → [self : Dvd α α → α → Prop , two_mul ]
#align even_iff_two_dvd even_iff_two_dvd
alias even_iff_two_dvd ↔ Even.two_dvd _
#align even.two_dvd Even.two_dvd
theorem Even.trans_dvd ( hm : Even m ) ( hn : m ∣ n ) : Even n :=
even_iff_two_dvd . 2 : ∀ {a b : Prop }, (a ↔ b b → a <| hm . two_dvd . trans : ∀ {α : Type ?u.66292} [inst : Semigroup α a b c : α }, a ∣ b b ∣ c a ∣ c hn
#align even.trans_dvd Even.trans_dvd
theorem Dvd.dvd.even ( hn : m ∣ n ) ( hm : Even m ) : Even n :=
hm . trans_dvd hn
#align has_dvd.dvd.even Dvd.dvd.even
@[ simp ]
theorem range_two_mul ( α ) [ Semiring α ] : ( Set.range : {α : Type ?u.66782} → {ι : Sort ?u.66781} → (ι → α Set α fun x : α => 2 * x ) = { a | Even a } := by
ext x
simp [ eq_comm : ∀ {α : Sort ?u.67283} {a b : α }, a = b ↔ b = a , two_mul , Even ]
#align range_two_mul range_two_mul
set_option linter.deprecated false in
@[ simp ] theorem even_bit0 ( a : α ) : Even ( bit0 : {α : Type ?u.71944} → [inst : Add α α → α a ) :=
⟨ a , rfl : ∀ {α : Sort ?u.72095} {a : α }, a = a ⟩
#align even_bit0 even_bit0
@[ simp ]
theorem even_two : Even ( 2 : α ) :=
⟨ 1 , by rw [ one_add_one_eq_two ] ⟩
#align even_two even_two
@[ simp ]
theorem Even.mul_left ( hm : Even m ) ( n ) : Even ( n * m ) :=
hm . map ( AddMonoidHom.mulLeft n )
#align even.mul_left Even.mul_left
@[ simp ]
theorem Even.mul_right : Even m ∀ (n : α ), Even (m * n Even.mul_right ( hm : Even m ) ( n ) : Even ( m * n ) :=
hm . map ( AddMonoidHom.mulRight n )
#align even.mul_right Even.mul_right
theorem even_two_mul ( m : α ) : Even ( 2 * m ) :=
⟨ m , two_mul _ ⟩
#align even_two_mul even_two_mul
theorem Even.pow_of_ne_zero : Even m ∀ {a : ℕ }, a ≠ 0 Even (m ^ a Even.pow_of_ne_zero ( hm : Even m ) : ∀ { a : ℕ }, a ≠ 0 → Even ( m ^ a )
| 0 , a0 => ( a0 rfl : ∀ {α : Sort ?u.74815} {a : α }, a = a ). elim
| a + 1, _ => by
rw [ pow_succ : ∀ {M : Type ?u.75012} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a * a ^ n ]
exact hm . mul_right _
#align even.pow_of_ne_zero Even.pow_of_ne_zero
section WithOdd
/-- An element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`. -/
def Odd ( a : α ) : Prop :=
∃ k , a = 2 * k + 1
#align odd Odd
set_option linter.deprecated false in
theorem odd_iff_exists_bit1 : ∀ {a : α }, Odd a ↔ ∃ b , a = bit1 b odd_iff_exists_bit1 { a : α } : Odd a ↔ ∃ b , a = bit1 : {α : Type ?u.75748} → [inst : One α [inst : Add α α → α b :=
exists_congr : ∀ {α : Sort ?u.75997} {p q : α → Prop (∀ (a : α ), p a ↔ q a ) → ((∃ a , p a ) ↔ ∃ a , q a ) fun b => by
rw [ two_mul ]
rfl
#align odd_iff_exists_bit1 odd_iff_exists_bit1
alias odd_iff_exists_bit1 ↔ Odd.exists_bit1 _
#align odd.exists_bit1 Odd.exists_bit1
set_option linter.deprecated false in
@[ simp ] theorem odd_bit1 ( a : α ) : Odd ( bit1 : {α : Type ?u.76163} → [inst : One α [inst : Add α α → α a ) :=
odd_iff_exists_bit1 . 2 : ∀ {a b : Prop }, (a ↔ b b → a ⟨ a , rfl : ∀ {α : Sort ?u.76398} {a : α }, a = a ⟩
#align odd_bit1 odd_bit1
@[ simp ]
theorem range_two_mul_add_one ( α : Type _ : Type (?u.76455+1)) [ Semiring α ] :
( Set.range : {α : Type ?u.76463} → {ι : Sort ?u.76462} → (ι → α Set α fun x : α => 2 * x + 1 ) = { a | Odd a } := by
ext x
simp [ Odd , eq_comm : ∀ {α : Sort ?u.77090} {a b : α }, a = b ↔ b = a ]
#align range_two_mul_add_one range_two_mul_add_one
theorem Even.add_odd : Even m → Odd n → Odd ( m + n ) := by
rintro ⟨ m , rfl ⟩ ⟨ n , rfl ⟩
exact ⟨ m + n , by rw [ mul_add , ← two_mul , add_assoc ] ⟩
#align even.add_odd Even.add_odd
theorem Odd.add_even ( hm : Odd m ) ( hn : Even n ) : Odd ( m + n ) := by
rw [ add_comm ]
exact hn . add_odd hm
#align odd.add_even Odd.add_even
theorem Odd.add_odd : Odd m → Odd n → Even ( m + n ) := by
rintro ⟨ m , rfl ⟩ ⟨ n , rfl ⟩
refine' ⟨ n + m + 1 , _ ⟩
rw [ two_mul , two_mul ]
ac_rfl
#align odd.add_odd Odd.add_odd
@[ simp ]
theorem odd_one : Odd ( 1 : α ) :=
⟨ 0 , ( zero_add _ ). symm : ∀ {α : Sort ?u.85508} {a b : α }, a = b b = a symm . trans : ∀ {α : Sort ?u.85515} {a b c : α }, a = b b = c a = c trans ( congr_arg : ∀ {α : Sort ?u.85530} {β : Sort ?u.85529} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ (· + (1 : α )) ( mul_zero _ ). symm : ∀ {α : Sort ?u.85899} {a b : α }, a = b b = a symm )⟩
#align odd_one odd_one
@[ simp ]
theorem odd_two_mul_add_one ( m : α ) : Odd ( 2 * m + 1 ) :=
⟨ m , rfl : ∀ {α : Sort ?u.86590} {a : α }, a = a ⟩
#align odd_two_mul_add_one odd_two_mul_add_one
theorem Odd.map [ RingHomClass F α β ] ( f : F ) : Odd m → Odd ( f m ) := by
rintro ⟨ m , rfl ⟩
exact ⟨ f m , by ↑f (2 * m + 1 = 2 * ↑f m + 1 simp [ two_mul ] ⟩
#align odd.map Odd.map
@[ simp ]
theorem Odd.mul : Odd m → Odd n → Odd ( m * n ) := by
rintro ⟨ m , rfl ⟩ ⟨ n , rfl ⟩
refine' ⟨ 2 * m * n + n + m , _ : ?m.89231 (2 * m * n + n + m ⟩
rw [ mul_add , add_mul , mul_one ,