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) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
Neil Strickland, Aaron Anderson
! This file was ported from Lean 3 source module algebra.group_with_zero.divisibility
! leanprover-community/mathlib commit e8638a0fcaf73e4500469f368ef9494e495099b3
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GroupWithZero.Basic
import Mathlib.Algebra.Divisibility.Units
/-!
# Divisibility in groups with zero.
Lemmas about divisibility in groups and monoids with zero.
-/
variable { α : Type _ }
section SemigroupWithZero
variable [ SemigroupWithZero : Type ?u.16 → Type ?u.16 α ] { a : α }
theorem eq_zero_of_zero_dvd : 0 ∣ a a = 0 eq_zero_of_zero_dvd ( h : 0 ∣ a ) : a = 0 :=
Dvd.elim : ∀ {α : Type ?u.146} [inst : Semigroup α P : Prop } {a b : α }, a ∣ b (∀ (c : α ), b = a * c P ) → P h fun c H' => H' . trans : ∀ {α : Sort ?u.176} {a b c : α }, a = b b = c a = c ( zero_mul c )
#align eq_zero_of_zero_dvd eq_zero_of_zero_dvd
/-- Given an element `a` of a commutative semigroup with zero, there exists another element whose
product with zero equals `a` iff `a` equals zero. -/
@[ simp ]
theorem zero_dvd_iff : 0 ∣ a ↔ a = 0 zero_dvd_iff : 0 ∣ a ↔ a = 0 :=
⟨ eq_zero_of_zero_dvd , fun h => by
rw [ h ]
exact ⟨ 0 , by simp ⟩ ⟩
#align zero_dvd_iff zero_dvd_iff
@[ simp ]
theorem dvd_zero ( a : α ) : a ∣ 0 :=
Dvd.intro : ∀ {α : Type ?u.941} [inst : Semigroup α a b : α } (c : α ), a * c = b a ∣ b 0 ( by simp )
#align dvd_zero dvd_zero
end SemigroupWithZero
/-- Given two elements `b`, `c` of a `CancelMonoidWithZero` and a nonzero element `a`,
`a*b` divides `a*c` iff `b` divides `c`. -/
theorem mul_dvd_mul_iff_left [ CancelMonoidWithZero : Type ?u.1186 → Type ?u.1186 α ] { a b c : α } ( ha : a ≠ 0 ) :
a * b ∣ a * c ↔ b ∣ c :=
exists_congr : ∀ {α : Sort ?u.1464} {p q : α → Prop (∀ (a : α ), p a ↔ q a ) → ((∃ a , p a ) ↔ ∃ a , q a ) fun d => by rw [ mul_assoc , mul_right_inj' ha ]
#align mul_dvd_mul_iff_left mul_dvd_mul_iff_left
/-- Given two elements `a`, `b` of a commutative `CancelMonoidWithZero` and a nonzero
element `c`, `a*c` divides `b*c` iff `a` divides `b`. -/
theorem mul_dvd_mul_iff_right [ CancelCommMonoidWithZero : Type ?u.1630 → Type ?u.1630 α ] { a b c : α } ( hc : c ≠ 0 ) :
a * c ∣ b * c ↔ a ∣ b :=
exists_congr : ∀ {α : Sort ?u.1876} {p q : α → Prop (∀ (a : α ), p a ↔ q a ) → ((∃ a , p a ) ↔ ∃ a , q a ) fun d => by rw [ mul_right_comm , mul_left_inj' hc ]
#align mul_dvd_mul_iff_right mul_dvd_mul_iff_right
section CommMonoidWithZero
variable [ CommMonoidWithZero : Type ?u.2239 → Type ?u.2239 α ]
/-- `DvdNotUnit a b` expresses that `a` divides `b` "strictly", i.e. that `b` divided by `a`
is not a unit. -/
def DvdNotUnit ( a b : α ) : Prop :=
a ≠ 0 ∧ ∃ x , ¬ IsUnit x ∧ b = a * x
#align dvd_not_unit DvdNotUnit
theorem dvdNotUnit_of_dvd_of_not_dvd : ∀ {a b : α }, a ∣ b ¬ b ∣ a DvdNotUnit a b dvdNotUnit_of_dvd_of_not_dvd { a b : α } ( hd : a ∣ b ) ( hnd : ¬ b ∣ a ) : DvdNotUnit a b := by
constructor
· rintro rfl
exact hnd ( dvd_zero _ )
· rcases hd with ⟨ c , rfl ⟩
refine' ⟨ c , _ , rfl : ∀ {α : Sort ?u.2456} {a : α }, a = a ⟩
rintro ⟨ u , rfl ⟩
simp at hnd
#align dvd_not_unit_of_dvd_of_not_dvd dvdNotUnit_of_dvd_of_not_dvd
end CommMonoidWithZero
theorem dvd_and_not_dvd_iff [ CancelCommMonoidWithZero : Type ?u.2786 → Type ?u.2786 α ] { x y : α } :
x ∣ y ∧ ¬ y ∣ x ↔ DvdNotUnit x y :=
⟨ fun ⟨⟨ d , hd ⟩, hyx ⟩ =>
⟨ fun hx0 => by simp [ hx0 ] at hyx ,
⟨ d , mt : ∀ {a b : Prop }, (a → b ¬ b ¬ a isUnit_iff_dvd_one . 1 : ∀ {a b : Prop }, (a ↔ b a → b fun ⟨ e , he ⟩ => hyx ⟨ e , by rw [ hd , mul_assoc , ← he , mul_one ] ⟩,
hd ⟩⟩,
fun ⟨ hx0 , d , hdu , hdx ⟩ =>
⟨⟨ d , hdx ⟩, fun ⟨ e , he ⟩ =>
hdu
( isUnit_of_dvd_one
⟨ e , mul_left_cancel₀ hx0 <| by conv =>
lhs
rw [ he , hdx ]
simp [ mul_assoc ] ⟩)⟩⟩
#align dvd_and_not_dvd_iff dvd_and_not_dvd_iff
section MonoidWithZero
variable [ MonoidWithZero : Type ?u.4185 → Type ?u.4185 α ]
theorem ne_zero_of_dvd_ne_zero : ∀ {p q : α }, q ≠ 0 p ∣ q p ≠ 0 ne_zero_of_dvd_ne_zero { p q : α } ( h₁ : q ≠ 0 ) ( h₂ : p ∣ q ) : p ≠ 0 := by
rcases h₂ with ⟨ u , rfl ⟩
exact left_ne_zero_of_mul : ∀ {M₀ : Type ?u.4323} [inst : MulZeroClass M₀ a b : M₀ }, a * b ≠ 0 a ≠ 0 h₁
#align ne_zero_of_dvd_ne_zero ne_zero_of_dvd_ne_zero
end MonoidWithZero
section CancelCommMonoidWithZero
variable [ CancelCommMonoidWithZero : Type ?u.5525 → Type ?u.5525 α ] [ Subsingleton α ˣ] { a b : α }
theorem dvd_antisymm : a ∣ b b ∣ a a = b dvd_antisymm : a ∣ b → b ∣ a → a = b := by
rintro ⟨ c , rfl ⟩ ⟨ d , hcd ⟩
rw [ mul_assoc , eq_comm : ∀ {α : Sort ?u.4700} {a b : α }, a = b ↔ b = a , mul_right_eq_self₀ , mul_eq_one ] at hcd
obtain ⟨ rfl , - ⟩ ⟨rfl, -⟩ | rfl : c = 1 ∧ d = 1 ∨ a = 0 rfl := hcd : c = 1 ∧ d = 1 ∨ a = 0 hcd intro.intro.inl.intro intro.intro.inr <;> intro.intro.inl.intro intro.intro.inr simp
#align dvd_antisymm dvd_antisymm
-- porting note: `attribute [protected]` is currently unsupported
-- attribute [protected] Nat.dvd_antisymm --This lemma is in core, so we protect it here
theorem dvd_antisymm' : a ∣ b → b ∣ a → b = a :=
flip : ∀ {α : Sort ?u.5217} {β : Sort ?u.5216} {φ : Sort ?u.5215}, (α → β → φ β → α → φ dvd_antisymm
#align dvd_antisymm' dvd_antisymm'
alias dvd_antisymm ← Dvd.dvd.antisymm
#align has_dvd.dvd.antisymm Dvd.dvd.antisymm
alias dvd_antisymm' ← Dvd.dvd.antisymm'
#align has_dvd.dvd.antisymm' Dvd.dvd.antisymm'
theorem eq_of_forall_dvd ( h : ∀ (c : α ), a ∣ c ↔ b ∣ c h : ∀ c , a ∣ c ↔ b ∣ c ) : a = b :=
(( h : ∀ (c : α ), a ∣ c ↔ b ∣ c h _ ). 2 : ∀ {a b : Prop }, (a ↔ b b → a dvd_rfl : ∀ {α : Type ?u.5400} [inst : Monoid α a : α }, a ∣ a ). antisymm <| ( h : ∀ (c : α ), a ∣ c ↔ b ∣ c h _ ). 1 : ∀ {a b : Prop }, (a ↔ b a → b dvd_rfl : ∀ {α : Type ?u.5496} [inst : Monoid α a : α }, a ∣ a
#align eq_of_forall_dvd eq_of_forall_dvd
theorem eq_of_forall_dvd' : (∀ (c : α ), c ∣ a ↔ c ∣ b ) → a = b eq_of_forall_dvd' ( h : ∀ (c : α ), c ∣ a ↔ c ∣ b h : ∀ c , c ∣ a ↔ c ∣ b ) : a = b :=
(( h : ∀ (c : α ), c ∣ a ↔ c ∣ b h _ ). 1 : ∀ {a b : Prop }, (a ↔ b a → b dvd_rfl : ∀ {α : Type ?u.5638} [inst : Monoid α a : α }, a ∣ a ). antisymm <| ( h : ∀ (c : α ), c ∣ a ↔ c ∣ b h _ ). 2 : ∀ {a b : Prop }, (a ↔ b b → a dvd_rfl : ∀ {α : Type ?u.5734} [inst : Monoid α a : α }, a ∣ a
#align eq_of_forall_dvd' eq_of_forall_dvd'
end CancelCommMonoidWithZero